Off-line Analysis
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/ […]
Author: Michael
- Website
- https://westergaard.eu/
- About Michael
- Time person of the year 2006, Nobel Peace Prize winner 2012.
Posts by Michael
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/ […]