Here we change the safety checker to do off-line analysis, thereby halving the execution time. MichaelTime person of the year 2006, Nobel Peace Prize winner 2012. westergaard.eu/ […]
Off-line Analysis
Tag: Model-checking
Graph Drawing and Export
Here we change the job to instead draw the state space graph. We modify the model to only contain two philosophers and play a bit with the resulting graph, including exporting it in DOT and GraphML format. MichaelTime person of the year 2006, Nobel Peace Prize winner 2012. westergaard.eu/ […]
Creating Job for the Sweep-line Method
We modify the job created in our previous example to instead use the sweep-line method. MichaelTime person of the year 2006, Nobel Peace Prize winner 2012. westergaard.eu/ […]
Checking Properties Using the Sweep-line Method
In this example we use the sweep-line method to check a mutual exclusion property of the dining philosophers example. MichaelTime person of the year 2006, Nobel Peace Prize winner 2012. westergaard.eu/ […]
Read More… from Checking Properties Using the Sweep-line Method
Tutorial on ASAP
I'm currently working on a tutorial for ASAP, the tool I'm working on at work. The tutorial is a mixture of slides and video demonstrations. You can see the four videos, I've currently done below: MichaelTime person of the year 2006, Nobel Peace Prize winner 2012. westergaard.eu/ […]
Checking a Custom Safety Property
Here, we extend the example to also check a simple mutex property, that two philosophers next to each other cannot eat at the same time. MichaelTime person of the year 2006, Nobel Peace Prize winner 2012. westergaard.eu/ […]