Please disable Adblockers and enable JavaScript for domain CEWebS.cs.univie.ac.at! We have NO ADS, but they may interfere with some of our course material.

Workflow Verifikation

Aufgabe 1: Modellierung

Modellieren sie ihr Main als Petrinet. Verwenden Sie entweder ein E/C oder ein P/T Netz, je nachdem was nötig ist. Welches Netz haben Sie verwendet? 

Aufgabe 2: Analyse

Wählen Sie eine geeignete initiale Markierung und führen Sie eine Erreichbarkeitsanalyse durch. Ist das Modell Safe, Sound, Bounded, Live, und warum? (Welches States gibt’s, durch welche Zeilen werden Sie repräsentiert, welche Eigenschaften hat das Netz). 

Aufgabe 3: Woflan Modellierung & Analyse 1

Setzen sie Ihr Main in dem von Woflan («http://www.win.tue.nl/woflan/doku.php») unterstützen Format .tpn um (im Texteditor schreiben und als .tpn speichern).  
 
Beispiel:  
place "P_0" init 1;
place "P_1"; ...
trans "t_1"~"Something" in "P_0" “P_2” out "P_1" ;
...
 
Analysieren Sie nun das Netz mit Woflan. Dokumentieren Sie die verschiedenen Eigenschaften  
und Analyseergebnisse.  

Aufgabe 4: Woflan Modellierung & Analyse 2

Modifizieren Sie nun das Netz derart, dass es in der Woflan - Analyse Structural Sound ist. 
 
Abzugeben:  
 
Tools: Woflan ist in der VM installiert, ist aber auch sehr einfach unter Windows zu installieren. 

 

Aufgaben die nicht benotet werden - zum gemeinsam Machen und Üben

Verwenden Sie nur E/C oder P/T Netze, je nachdem was nötig ist.  

Aufgabe 1

Ein Buchhändler nimmt Buchbestellungen in seinem kleinen Laden entgegen. Sobald ein Kunde seinen Laden betritt nimmt er eine Bestellung entgegen. Während der Buchhändler das Buch im Regal sucht, wartet der Kunde geduldig. Sobald der Händler das Buch gefunden hat, informiert er den Kunden über den Preis. Der Kunde bezahlt und verlässt das Geschäft. Da der Laden klein ist, kann nur jeweils ein Kunde im Laden sein. Der Verkaufsvorgang wiederholt sich sooft ein Kunde im Laden ist. Modellieren Sie das Netz, unter Berücksichtigung des Buchhändlers und der Kunden. Welche Art von Netz ist das? 

Aufgabe 2

Modellieren Sie das Beispiel aus (Aufgabe 1) aus Sicht des einzigen Buches im Lager, und von Kunden. Das Buch wechselt zwischen Lager und Verkaufsraum hin und her. Wenn ein Kunde eintrifft wird das Buch aus dem Verkaufsraum geholt. Wenn, der Kunde sich für den Kauf entscheidet, wird das Buch verkauft, ansonsten wandert es in den Lager zurück. 
 
Modellieren Sie das Netz, unter Berücksichtigung des Buches und der Kunden. 

Aufgabe 3

Wählen Sie eine geeignete initiale Markierung und führen Sie eine Erreichbarkeitsanalyse für (Aufgabe 1) durch. Ist das Modell Safe, Sound, Bounded, Live, und warum? (Welches States gibt’s, durch welche Zeilen werden Sie repräsentiert, welche Eigenschaften hat das Netz). 

Aufgabe 4

Wählen Sie eine geeignete initiale Markierung und führen Sie eine Erreichbarkeitsanalyse für (Aufgabe 2) durch. Ist das Modell Safe, Sound, Bounded, Live, und warum? (Welches States gibt’s, durch welche Zeilen werden Sie repräsentiert). 
Letzte Änderung: 26.11.2015, 08:27 | 478 Worte