This directory contains an interface that presents DiVinE models as kripke* objects for Spot. The DiVinE model checker [http://anna.fi.muni.cz/divine/] has a specification language called DVE that makes it easy to model processes synchonizing through channels [http://anna.fi.muni.cz/divine/language.html]. A lot of models can be found in the BEEM database at http://anna.fi.muni.cz/models/ For efficient generation of the state space of the model, DiVinE compiles the DVE input into a dynamic library that contains anything needed to generate the state-space. The LTSmin people [http://fmt.cs.utwente.nl/tools/ltsmin/] have made a patched version of DiVinE that compiles a dynamic library with a very simple C interface (no C++) and extra information about state variables (name, type, possible values). We are using this interface, therefore you need to install their version of DiVinE in order to use Spot's DVE interface. Installation of DiVinE ====================== Use the following commands to compile and install the patched version of DiVinE. git clone http://fmt.cs.utwente.nl/tools/scm/divine2.git cd divine2 mkdir _build && cd _build cmake .. -DMURPHI=OFF -DHOARD=OFF -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=$HOME/usr make make install The CMAKE_INSTALL_PREFIX variable is the equivalent of the --prefix option of configure scripts. If you decide to install in $HOME/usr like I do, make sure that $HOME/usr/bin is in your PATH. If you omit the CMAKE_INSTALL_PREFIX setting, it will default to /usr/local. After installation, you can check that compilation works by running the following command on any DVE model. It should create a file model.dve2C (which is a dynamic library). divine compile --ltsmin model.dve Usage with Spot =============== The function load_dve2() defined in dve2.hh in this directory will accept "model.dve" or "model.dve2C" as file argument. In the former case, it will call "divine compile --ltsmin" if "model.dve2C" does not exist or is older. Then it will load "model.dve2C" dynamically. load_dve2() also requires a set of atomic propositions that should be observed in the model. These are usually the atomic propositions that occur in the formula to verify, but it might be a larger set. There are two kinds of atomic propositions, those that refer to the state of a process, and those that compare the value of a variable. Let's have some example on an excerpt of the beem-peterson.4.dve model included in this directory: byte pos[4]; byte step[4]; process P_0 { byte j=0, k=0; state NCS, CS, wait ,q2,q3; init NCS; trans NCS -> wait { effect j = 1; }, wait -> q2 { guard j < 4; effect pos[0] = j;}, q2 -> q3 { effect step[j-1] = 0, k = 0; }, q3 -> q3 { guard k < 4 && (k == 0 || pos[k] < j); effect k = k+1;}, q3 -> wait { guard step[j-1] != 0 || k == 4; effect j = j+1;}, wait -> CS { guard j == 4; }, CS -> NCS { effect pos[0] = 0;}; } The following atomic propositions could be used in LTL formula: P_0.CS Process P_0 is in state CS. "pos[3] < 3" Global variable pos[3] is less than 3. "P_0.j >= 2" Process P_0's variable j is greater or equal to 2. P_0.j This is equivalent to "P_0.j != 0". Comparisons operators available are "<", ">", ">=", "<=", "==", and "!=". The left operant should always be a variable and the right operand should always be a number, so you cannot write something like "P_0.j <= P_0.i". Because the LTL parser knows nothing about the details of the languages we interface with, every atomic proposition that cannot be express using only alphanumeric characters (plus `_' and `.') should be enclosed in double quote. Caveat: "P_0.j >= 2" and " P_0.j>=2" (watch the spaces!) are considered to be two distinct atomic propositions with the same semantics. Examples ======== Using the dve2check program built into this directory, we can verify that the critical section is accessed infinitely often by some processes using: % ./dve2check beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' 2239039 unique states visited 0 strongly connected components in search stack 11449204 transitions explored 1024245 items max in DFS search stack no accepting run found Process P_0 can starve, waiting to enter in critical section: % ./dve2check beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)' 2190 unique states visited 34 strongly connected components in search stack 4896 transitions explored 83 items max in DFS search stack an accepting run exists (use -C to print it) Variable pos[1] is not always < 3 (this formula makes no sense, it is just to demonstrate the use of double quote). % ./dve2check beem-peterson.4.dve '!G("pos[1] < 3")' 130 unique states visited 61 strongly connected components in search stack 132 transitions explored 130 items max in DFS search stack an accepting run exists (use -C to print it) Two state-compression techniques have been implemented as experiments. Prefer the -Z option if your model use only non-negative value less than 2^28, it is way faster than -z (which will work for all values). Activating state compression will often reduce runtime. Compare: % ./dve2check -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' 2239039 unique states visited 0 strongly connected components in search stack 11449204 transitions explored 1024245 items max in DFS search stack 122102 pages allocated for emptiness check no accepting run found | user time | sys. time | total | name | ticks % | ticks % | ticks % | n ------------------------------------------------------------------------------- loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1 parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1 reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1 running emptiness chec | 1222 100.0 | 18 100.0 | 1240 100.0 | 1 translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1 ------------------------------------------------------------------------------- TOTAL | 1222 100.0 | 18 100.0 | 1240 100.0 | % ./dve2check -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' 2239039 unique states visited 0 strongly connected components in search stack 11449204 transitions explored 1024245 items max in DFS search stack 78580 pages allocated for emptiness check no accepting run found | user time | sys. time | total | name | ticks % | ticks % | ticks % | n ------------------------------------------------------------------------------- loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1 parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1 reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1 running emptiness chec | 1051 100.0 | 10 100.0 | 1061 100.0 | 1 translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1 ------------------------------------------------------------------------------- TOTAL | 1051 100.0 | 10 100.0 | 1061 100.0 | It's a 15% speedup in this case, be the improvement can be more important on larger models.