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.
[Info]
Workflow Verification
If you learned something and improved your model after assignment 1 (even if you did not submit the changes), use the new and improved model here.
Assignment 2a: Modeling
Model your A as a Petrinet. Use an E/C OR a P/T Net, depending on what you deem necessary. Document which Net you used and why?
Assignment 2b: Analysis
Select a suitable initial marking, and do a manual (by hand) reachability analysis. Is your model safe, sound bounded or live? Why?
Document it by explaining which LINE in your reachability analysis leads to which conclusion.
Assignment 2c: Woflan Modeling and Analysis
Implement your A in Woflan («http://www.win.tue.nl/woflan/doku.php») as a .tpn file (write in a text editor and save as .tpn).
Example:
place "P_0" init 1;
place "P_1"; ...
trans "t_1"~"Something" in "P_0" “P_2” out "P_1" ;
...
Analyse your net mit Woflan. Document the properties, and show why they are different from your manual analysis.
Assignment 2d: Woflan Modeling and Analysis
Change your net so that it is structural sound and live in Wolflan (if it is not already).
Submit:
- Aufgabe 2a: 1 PDF with screenshot of the current Signavio Model, and a scan (or photo) of your hand drawn petri net.
- Aufgabe 2b: 1 PDF with screenshot of the current Signavio Model, Petrinet, and a table with the reachability analysis as seen in the slides.
- Aufgabe 2c: 1 PDF with screenshots and explanations, 1 TPN.
- Aufgabe 2d: 1 PDF with screenshots and explanations, 1 TPN.
Tools: Woflan is installed in the available VM, but you can also install it manually under Windows and Linux (via Wine).
Assignments that are not graded, but should be done BEFORE doing the above
Use only E/C or P/T Nets, select the necessary. These examples will be discussed in the course.
The examples are in German. Please post translations to the forum if you want to help other students.
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: 11.11.2020, 09:07 | 565 Worte