Using Promela To Model Non-Deterministic Finite-State-Automatons: Concurrent Systems And Operating Systems Assignment, TCD

Part 1

Using Promela to model non-deterministic finite-state-automatons was described in Lecture 16. In the archive, you will find the image for an example (EXAMPLE-NDFA.png) along with a PML file (ndfa4.pml) that implements that example. This has added print statements that make its behavior easier to observe. It has been set up to allow SPIN to search for all possible accepting sequences of exactly length 4.

To do this search you need to do the following step: spin -run -E -c0 -e ndfa4.pml

This will generate a number of trail files, of which the nth can be viewed using spin -tn ndfa4.pml. So, for example, the 3rd trail file can be viewed using spin -t3 ndfa4.pml.

Task-1

Create a pml file called final.pml, that models the NDFA shown in FINAL-NDFA.png, and that also can search for accepting sequences of length less than or equal to 4.

Base your answer on ndfa4.pml, leaving lines 1..4 and 38..42 intact.

For submission for Part-1 : final.pml

Part 2

Practical 4 involved adding process priorities to a simulation of xv6. Here you are asked to extend this to the dynamic priority used in Linux, as described in Lecture 23.

The simulation has changed (from Practical 4) as follows

• A global clock variable has been added (defs.h) and is used to track the time taken by processes in swtch().
• The process state has a number of new components (see struct proc declaration in file proc.h).
• The scheduler, in proc.c, does a regular pass over the processes to adjust their priorities, calling adjustpriority(p) for every process p.