Diskrete Mathematik, Serie 22

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

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:
- 4-Bit LFSR, mit Abgriffen an den beiden äusseren Registern 1 und 4,
- 4-Bit LFSR, mit Abgriffen an den beiden inneren Registern 2 und 3.
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
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
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