SLAP
In the linked download there are some examples under fdr-static-livelock-build>/examples where you can see the CSPM syntax of the assertion
assert:[static-livelock-free]
In the GUI of FDR there is a separate tab called StaticLivelock, similar to the tabs for Livelock, Deadlock, Determinism, etc. From this tab the user can also add and check processes for static livelock freedom.
SLAP configuration
(from the Options menu)
- SLAP Symbolic Engine
- specifies the underlying symbolic engine. The options are a SAT solver (MiniSAT 2.0), a BDD engine (CUDD) or running both in parallel and waiting for the first one to finish.
- SLAP Closure Algorithm
- determines which algorithm is used for computing the transitive closure of the transition relation of each sequential leaf process. The options are Floyd-Warshall, matrix multiplication or iterative squaring.
Download
- Linux (x86_64)
- fdr-static-livelock-9477bd2.tar.gz