From e75a73dfb15fd109ae037b65a72dd785d4f7add9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Mar 2011 10:01:21 +0100 Subject: [PATCH] Some documentation of about the dve2 interface. * iface/dve2/README: New file. * NEWS: Mention it. * THANKS: Add Michael Weber. --- ChangeLog | 8 +++ NEWS | 2 +- iface/dve2/README | 136 ++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 145 insertions(+), 1 deletion(-) create mode 100644 iface/dve2/README diff --git a/ChangeLog b/ChangeLog index ba4532115..9406170ff 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-03-07 Alexandre Duret-Lutz + + Some documentation of about the dve2 interface. + + * iface/dve2/README: New file. + * NEWS: Mention it. + * THANKS: Add Michael Weber. + 2011-03-06 Alexandre Duret-Lutz * iface/dve2/dve2.cc, iface/dve2/dve2check.cc: Cosmetic changes diff --git a/NEWS b/NEWS index e588f252e..b6fbe63cc 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,6 @@ New in spot 0.7.1a: - Nothing yet. + * Spot can read DiVinE models. See iface/dve2/README for details. New in spot 0.7.1 (2001-02-07): diff --git a/iface/dve2/README b/iface/dve2/README new file mode 100644 index 000000000..28734880c --- /dev/null +++ b/iface/dve2/README @@ -0,0 +1,136 @@ +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 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 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)