Bit-state Hashing in ASAP

In this video, we change our safety checker to use bit-state hashing (with double hashing). We also try to modify our sweep-line checker to use bit-state hashing together with the sweep-line method, but see that this is not possible (as the sweep-line requires a storage we can remove from, but double hashing does not allow that)." […]

Read More… from Bit-state Hashing in ASAP

Hash Compaction in ASAP

In this video, we change our safety checker to use hash compaction. We also modify our sweep-line checker to use hash compaction together with the sweep-line method. MichaelTime person of the year 2006, Nobel Peace Prize winner 2012. westergaard.eu/ […]

Read More… from Hash Compaction in ASAP

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/ […]

Read More… from Creating Job for the Sweep-line Method

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