Interstaatliche Hochschule für Technik Buchs NTB, STRTDiskrete Mathematik
Block Informatik«Datum»
Serie 22PLTL: Schaltungen mit der lwb

  1. In der Stunde habe ich Ihnen gezeigt, wie man ein 3-Bit linear rückgekoppeltes Schieberegister (LFSR) in PLTL formalisieren kann und gewisse Eigenschaften beweisen. Machen Sie dasselbe für ein:
      Zeichnen Sie auch hier erst ein mögliches Timing-Diagramm mit «show(...)», und versuchen Sie dann zu beweisen, dass wenn das LFSR nicht überall Null ist, dieser Zustand auch in Zukunft nicht eintreten wird.
     
    Lösung
     
  2. Stellen Sie in PLTL eine Formel für folgende Eigenschaft auf, und visualisieren Sie mit «show(...)»:
     
    Die Variable p ist wiederholt immer zwei Takte auf 0 und dann zwei Takte auf 1 (Blinklampe mit Periode 4).
     
    Lösung
     
  3. In der Stunde habe ich eine sehr einfache Ampelsteuerung demonstriert:
    > spezifikation := taste -> F gruen;
    > steuerung := taste -> X gruen;
    > ok := steuerung -> spezifikation;
    > provable(ok);
    
    Finden Sie eine noch einfachere Steuerung, welche diese Spezifikation erfüllt.
     
    Etwas realistischer ist folgende Spezifikation:
    > spezifikation := G( (taste -> F gruen) & F ~gruen );
    
    Schreiben Sie hierfür eine Steuerung, und beweisen Sie, dass diese die Spezifikation erfüllt. Tipp: Können Sie dies nicht nachweisen, dann lassen Sie sich ein Gegenbeispiel mit «show(~ok)» anzeigen.
     
    Lösung