From ddc424f5a3fc7a6642718a1c549776ecac0dee4b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 5 Jan 2016 10:26:32 +0100 Subject: [PATCH] move ltsmin tests to tests/ltsmin/ * spot/ltsmin/defs.in: Delete. * spot/ltsmin/README, spot/ltsmin/beem-peterson.4.dve, spot/ltsmin/check.test, spot/ltsmin/elevator2.1.pm, spot/ltsmin/finite.dve, spot/ltsmin/finite.pm, spot/ltsmin/finite.test, spot/ltsmin/finite2.test, spot/ltsmin/kripke.test, spot/ltsmin/modelcheck.cc: Move... * tests/ltsmin/: ... here. * spot/ltsmin/README: Point to tests/ltsmin/README. * README, configure.ac, spot/ltsmin/Makefile.am, tests/.gitignore, tests/Makefile.am, tests/core/defs.in: Adjust. --- README | 3 +- configure.ac | 2 +- spot/ltsmin/Makefile.am | 19 -- spot/ltsmin/README | 197 +------------------- spot/ltsmin/defs.in | 89 --------- tests/.gitignore | 1 + tests/Makefile.am | 63 +++++-- tests/core/defs.in | 8 +- tests/ltsmin/.gitignore | 2 + tests/ltsmin/README | 201 +++++++++++++++++++++ {spot => tests}/ltsmin/beem-peterson.4.dve | 0 {spot => tests}/ltsmin/check.test | 0 {spot => tests}/ltsmin/elevator2.1.pm | 0 {spot => tests}/ltsmin/finite.dve | 0 {spot => tests}/ltsmin/finite.pm | 0 {spot => tests}/ltsmin/finite.test | 0 {spot => tests}/ltsmin/finite2.test | 0 {spot => tests}/ltsmin/kripke.test | 4 +- {spot => tests}/ltsmin/modelcheck.cc | 0 19 files changed, 264 insertions(+), 325 deletions(-) delete mode 100644 spot/ltsmin/defs.in create mode 100644 tests/ltsmin/.gitignore create mode 100644 tests/ltsmin/README rename {spot => tests}/ltsmin/beem-peterson.4.dve (100%) rename {spot => tests}/ltsmin/check.test (100%) rename {spot => tests}/ltsmin/elevator2.1.pm (100%) rename {spot => tests}/ltsmin/finite.dve (100%) rename {spot => tests}/ltsmin/finite.pm (100%) rename {spot => tests}/ltsmin/finite.test (100%) rename {spot => tests}/ltsmin/finite2.test (100%) rename {spot => tests}/ltsmin/kripke.test (89%) rename {spot => tests}/ltsmin/modelcheck.cc (100%) diff --git a/README b/README index e4c0b71bb..d654d35b0 100644 --- a/README +++ b/README @@ -151,8 +151,9 @@ spot/ Sources for libspot. sanity/ Sanity tests for the whole project. bin/ Command-line tools built on top of libspot. man/ Man pages for the above tools. -tests/ Test suite +tests/ Test suite. core/ Tests for libspot and the binaries. + ltsmin/ Tests for the DiVinE2/SpinS interface. python/ Tests for Python bindings. doc/ Documentation for Spot. org/ Source of userdoc/ as org-mode files. diff --git a/configure.ac b/configure.ac index bd0f02556..c713cf24b 100644 --- a/configure.ac +++ b/configure.ac @@ -203,7 +203,6 @@ AC_CONFIG_FILES([ lib/Makefile spot/graph/Makefile spot/kripke/Makefile - spot/ltsmin/defs spot/ltsmin/Makefile spot/Makefile spot/misc/Makefile @@ -220,6 +219,7 @@ AC_CONFIG_FILES([ python/ajax/Makefile python/Makefile tests/core/defs + tests/ltsmin/defs:tests/core/defs.in tests/Makefile tools/x-to-1 ]) diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am index 10374ef48..be0215a1d 100644 --- a/spot/ltsmin/Makefile.am +++ b/spot/ltsmin/Makefile.am @@ -31,22 +31,3 @@ libspotltsmin_la_LIBADD = \ $(top_builddir)/ltdl/libltdlc.la -lpthread libspotltsmin_la_LDFLAGS = -no-undefined $(SYMBOLIC_LDFLAGS) libspotltsmin_la_SOURCES = ltsmin.cc - -noinst_PROGRAMS = modelcheck - -modelcheck_SOURCES = modelcheck.cc -modelcheck_LDADD = libspotltsmin.la - -check_SCRIPTS = defs - -TESTS = check.test finite.test finite2.test kripke.test -EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve finite.pm - -kripke.test: $(top_builddir)/tests/core/parse_print$(EXEEXT) - -$(top_builddir)/tests/core/parse_print$(EXEEXT): - cd $(top_builddir)/tests && \ - $(MAKE) $(AM_MAKEFLAGS) core/parse_print$(EXEEXT) - -distclean-local: - rm -rf $(TESTS:.test=.dir) diff --git a/spot/ltsmin/README b/spot/ltsmin/README index cd043a788..0b9a02e1b 100644 --- a/spot/ltsmin/README +++ b/spot/ltsmin/README @@ -1,198 +1,5 @@ This directory contains an interface that presents DiVinE and PROMELA 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/ - -The LTSmin people [http://fmt.cs.utwente.nl/tools/ltsmin/] patched -DiVinE and SpinJa to compile models as dynamic libraries. This dynamic -library provides a very simple C interface (no C++) and extra -information about state variables (name, type, possible values). We -use this interface so you will need to install their version of these -tools to use Spot with DVE or PROMELA models. - - - -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 - - -Installation of SpinS -====================== - -The extended version of SpinJa is called SpinS and should be included -with LTSmin. -You can download LTSmin from their website: -[http://fmt.cs.utwente.nl/tools/ltsmin/] and install it following the -INSTALL instructions. - -To compile a promela model, simply run the following command: - spins model.pm - -It should create a dynamic library called model.pm.spins in the -current directory. - - -Usage with Spot -=============== - - The function load_dve2() defined in dve2.hh in this directory will - accept either a model or its compiled version as file argument. In - the former case, it will call "divine compile --ltsmin model.dve" or - "spins model.pm" depending on the file extension, only if a compiled - model with the corresponding file extension (.dve2C or .spins) does - not exist or is older. Then it will load the compiled model - 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". - - Comparison operators available are "<", ">", ">=", "<=", "==", and - "!=". The left operand 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 - expressed 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 modelcheck program built into this directory, we can verify - that the critical section is accessed infinitely often by some - processes using: - - % ./modelcheck 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: - - % ./modelcheck 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). - - % ./modelcheck 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: - -% ./modelcheck -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 | - -% ./modelcheck -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. +For usage and installation instructions, see the README in +tests/ltsmin/README. diff --git a/spot/ltsmin/defs.in b/spot/ltsmin/defs.in deleted file mode 100644 index 2be5471e9..000000000 --- a/spot/ltsmin/defs.in +++ /dev/null @@ -1,89 +0,0 @@ -# -*- shell-script -*- -# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -# Ensure we are running from the right directory. -test -f ./defs || { - echo "defs: not found in current directory" 1>&2 - exit 1 -} - -# If srcdir is not set, then we are not running from `make check'. -if test -z "$srcdir"; then - # compute $srcdir. - srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'` - test $srcdir = $0 && srcdir=. -fi - -# Ensure $srcdir is set correctly. -test -f $srcdir/defs.in || { - echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 - exit 1 -} - -echo "== Running test $0" - -me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'` - -testSubDir=$me.dir -chmod -R a+rwx $testSubDir > /dev/null 2>&1 -rm -rf $testSubDir > /dev/null 2>&1 -mkdir $testSubDir -cd $testSubDir - -# Adjust srcdir now that we are in a subdirectory. We still want to -# source directory corresponding to the build directory that contains -# $testSubDir. -case $srcdir in - # I - [\\/$]* | ?:[\\/]* );; - *) srcdir=../$srcdir -esac - -DOT='@DOT@' -top_builddir='../@top_builddir@' -LBTT="@LBTT@" -LBTT_TRANSLATE="@LBTT_TRANSLATE@" -VALGRIND='@VALGRIND@' -SPIN='@SPIN@' -LTL2BA='@LTL2BA@' - -run() -{ - expected_exitcode=$1 - shift - exitcode=0 - if test -n "$VALGRIND"; then - exec 6>valgrind.err - GLIBCPP_FORCE_NEW=1 \ - ../../../libtool --mode=execute \ - $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" || - exitcode=$? - cat valgrind.err 1>&2 - test -z "`sed 1q valgrind.err`" || exit 50 - rm -f valgrind.err - else - "$@" || exitcode=$? - fi - test $exitcode = $expected_exitcode || exit 1 -} - -set -x diff --git a/tests/.gitignore b/tests/.gitignore index ae88eb6a6..b8936f1f7 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -1 +1,2 @@ *.dir +run diff --git a/tests/Makefile.am b/tests/Makefile.am index 82e512a0a..e26a8b00b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -1,6 +1,7 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de -## Recherche et Développement de l'Epita (LRDE). + +## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 +## Laboratoire de Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -25,17 +26,33 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = $(top_builddir)/spot/libspot.la -# These are the most used test programs, and they are also useful -# to run manually outside the test suite. Always build them. -noinst_PROGRAMS = core/ikwiad core/randtgba - TEST_EXTENTIONS = .test .py .ipynb LOG_COMPILER = ./run TEST_LOG_COMPILER = ./run LOG_DRIVER = $(TEST_LOG_DRIVER) # ensure run is rebuilt before the tests are run. -check_SCRIPTS = run core/defs +check_SCRIPTS = run + +# We try to keep this somehow by strength. Test basic things first, +# because such failures will be easier to diagnose and fix. +TESTS = $(TESTS_tl) $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa) \ + $(TESTS_python) $(TESTS_ltsmin) + +distclean-local: + rm -rf $(TESTS:.test=.dir) + + +############################## CORE ############################## + +check_SCRIPTS += core/defs + +core/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in + $(top_builddir)/config.status --file core/defs + +# These are the most used test programs, and they are also useful +# to run manually outside the test suite. Always build them. +noinst_PROGRAMS = core/ikwiad core/randtgba # Keep this sorted alphabetically. check_PROGRAMS = \ @@ -120,10 +137,6 @@ core_tunenoform_SOURCES = core/equalsf.cc core_tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"' -# Keep this sorted by STRENGTH. Test basic things first, -# because such failures will be easier to diagnose and fix. -TESTS = $(TESTS_tl) $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa) $(TESTS_python) - TESTS_tl = \ core/bare.test \ core/parse.test \ @@ -255,8 +268,8 @@ TESTS_twa = \ core/randpsl.test \ core/cycles.test -distclean-local: - rm -rf $(TESTS:.test=.dir) + +############################## PYTHON ############################## TESTS_python = \ python/acc_cond.ipynb \ @@ -294,8 +307,30 @@ SUFFIXES = .ipynb .html .PHONY: nb-html nb-html: $(TESTS_python:.ipynb=.html) - EXTRA_DIST = \ $(TESTS) \ python/ltl2tgba.py \ python/ipnbdoctest.py + + +############################## LTSMIN ############################## + +noinst_PROGRAMS += ltsmin/modelcheck + +ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc +ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la + +check_SCRIPTS += ltsmin/defs + +ltsmin/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in + $(top_builddir)/config.status --file ltsmin/defs:core/defs.in + +TESTS_ltsmin = \ + ltsmin/check.test \ + ltsmin/finite.test \ + ltsmin/finite2.test \ + ltsmin/kripke.test + +EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/finite.dve ltsmin/finite.pm + +ltlsmin/kripke.log: core/parse_print$(EXEEXT) diff --git a/tests/core/defs.in b/tests/core/defs.in index 11a9fd540..7df6fdf77 100644 --- a/tests/core/defs.in +++ b/tests/core/defs.in @@ -33,9 +33,9 @@ if test -z "$srcdir"; then test $srcdir = $0 && srcdir=. fi -# Ensure $srcdir is set correctly. -test -f $srcdir/defs.in || { - echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 +# Ensure $srcdir is set correctly. It should point to a subdirectory of tests. +test -f $srcdir/../core/defs.in || { + echo "$srcdir/../core/defs.in not found, check \$srcdir" 1>&2 exit 1 } @@ -66,7 +66,7 @@ LTL2BA='@LTL2BA@' PYTHON='@PYTHON@' top_srcdir='@abs_top_srcdir@' -# The test cases assume these variable are undefined +# The test cases assume these variables are undefined unset SPOT_DOTEXTRA unset SPOT_DOTDEFAULT diff --git a/tests/ltsmin/.gitignore b/tests/ltsmin/.gitignore new file mode 100644 index 000000000..b3518bd8b --- /dev/null +++ b/tests/ltsmin/.gitignore @@ -0,0 +1,2 @@ +defs +modelcheck diff --git a/tests/ltsmin/README b/tests/ltsmin/README new file mode 100644 index 000000000..5e16fea5f --- /dev/null +++ b/tests/ltsmin/README @@ -0,0 +1,201 @@ +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/ + +The LTSmin group [http://fmt.cs.utwente.nl/tools/ltsmin/] patched +DiVinE and SpinJa to compile models as dynamic libraries. This dynamic +library provides a very simple C interface (no C++) and extra +information about state variables (name, type, possible values). We +use this interface so you will need to install their version of these +tools to use Spot with DVE or PROMELA models. + +The source code for our interface is in spot/ltsmin/ and generate a +separate library, libspotltsmin.so, that has to be loaded in addition +to libspot.so. The current directory contains some testing code based +on a toy modelchecker built upon the above interface: using it require +an installation of DiVinE or SpinS (preferably both for testing +purpose). + + +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 + + +Installation of SpinS +====================== + +The extended version of SpinJa is called SpinS and should be included +with LTSmin. +You can download LTSmin from their website: +[http://fmt.cs.utwente.nl/tools/ltsmin/] and install it following the +INSTALL instructions. + +To compile a promela model, simply run the following command: + spins model.pm + +It should create a dynamic library called model.pm.spins in the +current directory. + + +Usage with Spot +=============== + + The function load_dve2() defined in dve2.hh in this directory will + accept either a model or its compiled version as file argument. In + the former case, it will call "divine compile --ltsmin model.dve" or + "spins model.pm" depending on the file extension, only if a compiled + model with the corresponding file extension (.dve2C or .spins) does + not exist or is older. Then it will load the compiled model + 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". + + Comparison operators available are "<", ">", ">=", "<=", "==", and + "!=". The left operand 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 + expressed 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 modelcheck program built into this directory, we can verify + that the critical section is accessed infinitely often by some + processes using: + + % ./modelcheck 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: + + % ./modelcheck 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). + + % ./modelcheck 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: + +% ./modelcheck -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 | + +% ./modelcheck -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. diff --git a/spot/ltsmin/beem-peterson.4.dve b/tests/ltsmin/beem-peterson.4.dve similarity index 100% rename from spot/ltsmin/beem-peterson.4.dve rename to tests/ltsmin/beem-peterson.4.dve diff --git a/spot/ltsmin/check.test b/tests/ltsmin/check.test similarity index 100% rename from spot/ltsmin/check.test rename to tests/ltsmin/check.test diff --git a/spot/ltsmin/elevator2.1.pm b/tests/ltsmin/elevator2.1.pm similarity index 100% rename from spot/ltsmin/elevator2.1.pm rename to tests/ltsmin/elevator2.1.pm diff --git a/spot/ltsmin/finite.dve b/tests/ltsmin/finite.dve similarity index 100% rename from spot/ltsmin/finite.dve rename to tests/ltsmin/finite.dve diff --git a/spot/ltsmin/finite.pm b/tests/ltsmin/finite.pm similarity index 100% rename from spot/ltsmin/finite.pm rename to tests/ltsmin/finite.pm diff --git a/spot/ltsmin/finite.test b/tests/ltsmin/finite.test similarity index 100% rename from spot/ltsmin/finite.test rename to tests/ltsmin/finite.test diff --git a/spot/ltsmin/finite2.test b/tests/ltsmin/finite2.test similarity index 100% rename from spot/ltsmin/finite2.test rename to tests/ltsmin/finite2.test diff --git a/spot/ltsmin/kripke.test b/tests/ltsmin/kripke.test similarity index 89% rename from spot/ltsmin/kripke.test rename to tests/ltsmin/kripke.test index 383778a6f..50e5b9973 100755 --- a/spot/ltsmin/kripke.test +++ b/tests/ltsmin/kripke.test @@ -34,9 +34,9 @@ fi set -e run 0 ../modelcheck -gK $srcdir/finite.dve 'F("P.a > 5")' > output -run 0 $top_builddir/tests/core/parse_print output | tr -d '"' > output2 +run 0 ../../core/parse_print output | tr -d '"' > output2 tr -d '"' < output >outputF cmp outputF output2 ../modelcheck -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP -$top_builddir/tests/core/ikwiad -e -KPoutputP '!G("pos[1] < 3")' +../../core/ikwiad -e -KPoutputP '!G("pos[1] < 3")' diff --git a/spot/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc similarity index 100% rename from spot/ltsmin/modelcheck.cc rename to tests/ltsmin/modelcheck.cc