Commit 1ea046a5 authored by Etienne Renault's avatar Etienne Renault

modelcheck: rewrite and use argp

* tests/Makefile.am, tests/ltsmin/check.test,
tests/ltsmin/finite.test, tests/ltsmin/finite2.test,
tests/ltsmin/kripke.test, tests/ltsmin/modelcheck.cc: here.
parent 975a9aca
......@@ -454,10 +454,14 @@ EXTRA_DIST = \
if USE_LTSMIN
check_PROGRAMS += ltsmin/modelcheck
ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \
$(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib
ltsmin_modelcheck_SOURCES = ltsmin/modelcheck.cc
ltsmin_modelcheck_LDADD = $(top_builddir)/spot/ltsmin/libspotltsmin.la \
$(LDADD) -lpthread
ltsmin_modelcheck_LDADD = \
$(top_builddir)/bin/libcommon.a \
$(top_builddir)/lib/libgnu.la \
$(top_builddir)/spot/libspot.la \
$(top_builddir)/spot/ltsmin/libspotltsmin.la
check_SCRIPTS += ltsmin/defs
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche
# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2017 Laboratoire de Recherche
# et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -32,37 +32,43 @@ fi
set -e
for opt in '' '-z'; do
# Promela
for opt in '' '--compress 1'; do
run 0 ../modelcheck --is-emtpy $opt --model $srcdir/elevator2.1.pm \
--formula '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
run 1 ../modelcheck --is-empty $opt --model $srcdir/elevator2.1.pm \
--formula 'F("p==2")'
done
# dve2
for opt in '' '--compress 1'; do
# The three examples from the README.
# (Don't run the first one using "run 0" because it would take too much
# time with valgrind.).
../modelcheck $opt -E $srcdir/beem-peterson.4.dve \
'!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
| grep -v pages > stdout1
../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
--formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
| grep -v pages > stdout1
# same formula, different syntax.
../modelcheck $opt -E $srcdir/beem-peterson.4.dve \
'!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \
| grep -v pages > stdout2
../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
--formula '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \
| grep -v pages > stdout2
cmp stdout1 stdout2
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve \
'!G(P_0.wait -> F P_0.CS)'
run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve \
--formula '!G(P_0.wait -> F P_0.CS)'
run 1 ../modelcheck --is-empty $opt --model $srcdir/beem-peterson.4.dve\
--formula '!G("pos[1] < 3")'
done
# Now check some error messages.
run 1 ../modelcheck foo.dve "F(P_0.CS)" 2>stderr
run 2 ../modelcheck --model foo.dve --formula "F(P_0.CS)" 2>stderr
cat stderr
grep 'Cannot open' stderr
# the dve2C file was generated in the current directory
run 1 ../modelcheck beem-peterson.4.dve2C \
'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
run 2 ../modelcheck --model beem-peterson.4.dve2C \
--formula 'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
cat stderr
grep 'variable `foo' stderr
grep "state \`f'.*P_0" stderr
grep "Unexpected.*\`xx'" stderr
grep 'Possible.*CS' stderr
grep 'Possible.*NCS' stderr
grep 'Possible.*q2' stderr
grep 'Possible.*q3' stderr
grep 'Possible.*wait' stderr
grep 'Proposition "foo"' stderr
grep 'Proposition "P_0.f"' stderr
grep 'Proposition "P_0.k<2xx"' stderr
......@@ -31,28 +31,33 @@ else
fi
set -e
run 0 ../modelcheck -gm $srcdir/finite.dve '"P.a < 10"' > stdout
run 0 ../modelcheck --dot=model --model $srcdir/finite.dve \
--formula '"P.a < 10"' > stdout
test `grep ' -> ' stdout | wc -l` = 25
test `grep 'P.a=' stdout | wc -l` = 15
run 0 ../modelcheck -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2
run 0 ../modelcheck --selfloopize true --dot=model --model $srcdir/finite.dve \
--formula '"P.a < 10"' > stdout2
cmp stdout stdout2
run 0 ../modelcheck -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
run 0 ../modelcheck --selfloopize false --dot model --model $srcdir/finite.dve \
--formula '"P.a < 10"' > stdout
test `grep ' -> ' stdout | wc -l` = 19
test `grep 'P.a=' stdout | wc -l` = 15
# the same with compressed states
run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
run 0 ../modelcheck --compress 1 --selfloopize false \
--dot model --model $srcdir/finite.dve --formula '"P.a < 10"' > stdout
test `grep ' -> ' stdout | wc -l` = 19
test `grep 'P.a=' stdout | wc -l` = 15
run 0 ../modelcheck -ddead -E $srcdir/finite.dve \
'!(G(dead -> ("P.a==3" | "P.b==3")))'
run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
--formula '!(G(dead -> ("P.a==3" | "P.b==3")))'
run 0 ../modelcheck -ddead -e $srcdir/finite.dve \
'!(G(dead -> ("P.a==2" | "P.b==3")))'
run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
--formula '!(G(dead -> ("P.a==2" | "P.b==3")))'
# This used to segfault because of a bug in a
# function that do not exist anymore.
run 0 ../modelcheck -gp $srcdir/finite.dve true
run 0 ../modelcheck --dot product --model $srcdir/finite.dve \
--formula true
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement
# Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -28,27 +28,30 @@ if ! spins $srcdir/finite.pm; then
exit 77
fi
run 0 ../modelcheck -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout
run 0 ../modelcheck --dot model --model $srcdir/finite.pm \
--formula '"P_0.a < 10"' > stdout
test `grep ' -> ' stdout | wc -l` = 25
test `grep 'P_0.a=' stdout | wc -l` = 15
run 0 ../modelcheck -dtrue -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout2
run 0 ../modelcheck --selfloopize true --dot model --model $srcdir/finite.pm \
--formula '"P_0.a < 10"' > stdout2
diff stdout stdout2
run 0 ../modelcheck -dfalse -gm $srcdir/finite.pm '"P_0.a < 10"' > stdout
run 0 ../modelcheck --selfloopize dfalse --dot model --model $srcdir/finite.pm \
--formula '"P_0.a < 10"' > stdout
test `grep ' -> ' stdout | wc -l` = 19
test `grep 'P_0.a=' stdout | wc -l` = 15
# the same with compressed states
run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.pm '"P_0.a < 10"' \
> stdout
run 0 ../modelcheck -compress --selfloopize false --dot model \
--model $srcdir/finite.pm --formula '"P_0.a < 10"' > stdout
test `grep ' -> ' stdout | wc -l` = 19
test `grep 'P_0.a=' stdout | wc -l` = 15
run 0 ../modelcheck -ddead -E $srcdir/finite.pm \
'!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \
--formula '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
run 0 ../modelcheck -ddead -e $srcdir/finite.pm \
'!(G(dead -> ("P_0.a==2" | "P_0.b==3")))'
run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.pm \
--formula '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))'
run 0 ../modelcheck -gp $srcdir/finite.pm true
run 0 ../modelcheck --dot product --model $srcdir/finite.pm --formula true
#! /bin/sh
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement
# Copyright (C) 2011, 2014, 2015, 2016 Laboratoire de Recherche et Developpement
# de l'Epita (LRDE)
#
# This file is part of Spot, a model checking library.
......@@ -33,10 +33,12 @@ fi
set -e
run 0 ../modelcheck -gK $srcdir/finite.dve 'F("P.a > 5")' > output
run 0 ../modelcheck --kripke --model $srcdir/finite.dve \
--formula 'F("P.a > 5")' > output
run 0 ../../core/kripkecat output | tr -d '"' > output2
tr -d '"' < output >outputF
cmp outputF output2
../modelcheck -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP
../modelcheck --kripke --model $srcdir/beem-peterson.4.dve \
--formula '!G("pos[1] < 3")' > outputP
../../core/ikwiad -e -KPoutputP '!G("pos[1] < 3")'
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment