Merge kripketest, graphtest and ltltest into tests
* README, configure.ac, iface/ltsmin/Makefile.am, src/tests/defs.in, src/tests/.gitignore, src/tests/Makefile.am, src/Makefile.am: update references. * src/kripketest/.gitignore, src/kripketest/Makefile.am, src/kripketest/defs.in, src/graphtest/.gitignore, src/graphtest/Makefile.am, src/graphtest/defs.in, src/ltltest/.cvsignore, src/ltltest/.gitignore, src/ltltest/Makefile.am, src/ltltest/defs.in:: remove files. * src/kripketest/bad_parsing.test, src/kripketest/kripke.test, src/kripketest/origin, src/kripketest/parse_print_test.cc, src/ltltest/bare.test, src/ltltest/consterm.cc, src/ltltest/consterm.test, src/tests/defs.in, src/ltltest/equals.test, src/ltltest/equalsf.cc, src/ltltest/eventuniv.test, src/ltltest/exclusive-ltl.test, src/graphtest/graph.cc, src/graphtest/graph.test, src/ltltest/isop.test, src/ltltest/kind.cc, src/ltltest/kind.test, src/ltltest/latex.test, src/ltltest/lbt.test, src/ltltest/length.cc, src/ltltest/length.test, src/ltltest/lenient.test, src/ltltest/ltlcrossgrind.test, src/ltltest/ltlfilt.test, src/ltltest/ltlgrind.test, src/ltltest/ltlrel.cc, src/ltltest/ltlrel.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/graphtest/ngraph.cc, src/graphtest/ngraph.test, src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/rand.test, src/ltltest/readltl.cc, src/ltltest/reduc.cc, src/ltltest/reduc.test, src/ltltest/reduc0.test, src/ltltest/reduccmp.test, src/ltltest/reducpsl.test, src/ltltest/remove_x.test, src/ltltest/stutter-ltl.test, src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test, src/graphtest/tgbagraph.test, src/ltltest/tostring.cc, src/ltltest/tostring.test, src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test, src/graphtest/twagraph.cc, src/ltltest/unabbrevwm.test,src/ltltest/utf8.test, src/ltltest/uwrm.test: rename as... * src/tests/bad_parsing.test, src/tests/kripke.test, src/tests/origin, src/tests/parse_print_test.cc, src/tests/bare.test, src/tests/consterm.cc, src/tests/consterm.test, src/tests/equals.test, src/tests/equalsf.cc, src/tests/eventuniv.test, src/tests/exclusive-ltl.test, src/tests/graph.cc, src/tests/graph.test, src/tests/isop.test, src/tests/kind.cc, src/tests/kind.test, src/tests/latex.test, src/tests/lbt.test, src/tests/length.cc, src/tests/length.test, src/tests/lenient.test, src/tests/ltlcrossgrind.test, src/tests/ltlfilt.test, src/tests/ltlgrind.test, src/tests/ltlrel.cc, src/tests/ltlrel.test, src/tests/lunabbrev.test, src/tests/nenoform.test, src/tests/ngraph.cc, src/tests/ngraph.test, src/tests/parse.test, src/tests/parseerr.test, src/tests/rand.test, src/tests/readltl.cc, src/tests/reduc.cc, src/tests/reduc.test, src/tests/reduc0.test, src/tests/reduccmp.test, src/tests/reducpsl.test, src/tests/remove_x.test, src/tests/stutter-ltl.test, src/tests/syntimpl.cc, src/tests/syntimpl.test, src/tests/tgbagraph.test, src/tests/tostring.cc, src/tests/tostring.test, src/tests/tunabbrev.test, src/tests/tunenoform.test, src/tests/twagraph.cc, src/tests/unabbrevwm.test, src/tests/utf8.test, src/tests/uwrm.test: ...these!
This commit is contained in:
Etienne Renault
parent
bd57f7a991
commit
66bd8f34db
69 changed files with 137 additions and 522 deletions
29
src/tests/.gitignore
vendored
29
src/tests/.gitignore
vendored
|
|
@ -1,41 +1,70 @@
|
|||
acc
|
||||
apcollect
|
||||
bddprod
|
||||
bitvect
|
||||
blue_counter
|
||||
checkpsl
|
||||
checkta
|
||||
complement
|
||||
consterm
|
||||
defs
|
||||
.deps
|
||||
*.dot
|
||||
eltl2tgba
|
||||
emptchk
|
||||
defs
|
||||
equals
|
||||
expect
|
||||
expldot
|
||||
explicit
|
||||
explicit2
|
||||
explicit3
|
||||
explprod
|
||||
graph
|
||||
genltl
|
||||
input
|
||||
intvcomp
|
||||
intvcmp2
|
||||
kind
|
||||
length
|
||||
.libs
|
||||
ltl2tgba
|
||||
ltl2dot
|
||||
ltl2text
|
||||
ltlmagic
|
||||
ltlprod
|
||||
ltlrel
|
||||
lunabbrev
|
||||
Makefile
|
||||
Makefile.in
|
||||
maskacc
|
||||
mixprod
|
||||
nequals
|
||||
nenoform
|
||||
ngraph
|
||||
output1
|
||||
output2
|
||||
parse_print
|
||||
powerset
|
||||
*.ps
|
||||
randltl
|
||||
randtgba
|
||||
readsat
|
||||
readsave
|
||||
reduc
|
||||
reduceu
|
||||
reductau
|
||||
reductaustr
|
||||
reduccmp
|
||||
reductgba
|
||||
stdout
|
||||
spotlbtt
|
||||
syntimpl
|
||||
taatgba
|
||||
tgbagraph
|
||||
tgbaread
|
||||
tostring
|
||||
tripprod
|
||||
tunabbrev
|
||||
tunenoform
|
||||
unabbrevwm
|
||||
|
|
|
|||
|
|
@ -36,12 +36,34 @@ check_PROGRAMS = \
|
|||
complement \
|
||||
checkpsl \
|
||||
checkta \
|
||||
consterm \
|
||||
emptchk \
|
||||
equals \
|
||||
graph \
|
||||
kind \
|
||||
length \
|
||||
intvcomp \
|
||||
intvcmp2 \
|
||||
ltlprod \
|
||||
ltl2dot \
|
||||
ltl2text \
|
||||
ltlrel \
|
||||
lunabbrev \
|
||||
nequals \
|
||||
nenoform \
|
||||
ngraph \
|
||||
parse_print \
|
||||
readsat \
|
||||
taatgba
|
||||
reduc \
|
||||
reduccmp \
|
||||
reduceu \
|
||||
reductaustr \
|
||||
syntimpl \
|
||||
taatgba \
|
||||
tgbagraph \
|
||||
tostring \
|
||||
tunabbrev \
|
||||
tunenoform
|
||||
|
||||
# Keep this sorted alphabetically.
|
||||
acc_SOURCES = acc.cc
|
||||
|
|
@ -50,17 +72,93 @@ checkpsl_SOURCES = checkpsl.cc
|
|||
checkta_SOURCES = checkta.cc
|
||||
complement_SOURCES = complementation.cc
|
||||
emptchk_SOURCES = emptchk.cc
|
||||
graph_SOURCES = graph.cc
|
||||
intvcomp_SOURCES = intvcomp.cc
|
||||
intvcmp2_SOURCES = intvcmp2.cc
|
||||
ltl2tgba_SOURCES = ltl2tgba.cc
|
||||
ltlprod_SOURCES = ltlprod.cc
|
||||
ngraph_SOURCES = ngraph.cc
|
||||
parse_print_SOURCES = parse_print_test.cc
|
||||
randtgba_SOURCES = randtgba.cc
|
||||
readsat_SOURCES = readsat.cc
|
||||
taatgba_SOURCES = taatgba.cc
|
||||
tgbagraph_SOURCES = twagraph.cc
|
||||
consterm_SOURCES = consterm.cc
|
||||
equals_SOURCES = equalsf.cc
|
||||
kind_SOURCES = kind.cc
|
||||
length_SOURCES = length.cc
|
||||
ltl2dot_SOURCES = readltl.cc
|
||||
ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
|
||||
ltl2text_SOURCES = readltl.cc
|
||||
ltlrel_SOURCES = ltlrel.cc
|
||||
lunabbrev_SOURCES = equalsf.cc
|
||||
lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
|
||||
nenoform_SOURCES = equalsf.cc
|
||||
nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
|
||||
nequals_SOURCES = equalsf.cc
|
||||
nequals_CPPFLAGS = $(AM_CPPFLAGS) -DNEGATE
|
||||
reduc_SOURCES = reduc.cc
|
||||
reduccmp_SOURCES = equalsf.cc
|
||||
reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
|
||||
reduceu_SOURCES = equalsf.cc
|
||||
reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV
|
||||
reductaustr_SOURCES = equalsf.cc
|
||||
reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR
|
||||
syntimpl_SOURCES = syntimpl.cc
|
||||
tostring_SOURCES = tostring.cc
|
||||
tunabbrev_SOURCES = equalsf.cc
|
||||
tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
|
||||
tunenoform_SOURCES = equalsf.cc
|
||||
tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV
|
||||
|
||||
|
||||
# Keep this sorted by STRENGTH. Test basic things first,
|
||||
# because such failures will be easier to diagnose and fix.
|
||||
TESTS = $(TESTS_twa)
|
||||
TESTS = $(TESTS_ltl) $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa)
|
||||
|
||||
TESTS_ltl = \
|
||||
bare.test \
|
||||
parse.test \
|
||||
parseerr.test \
|
||||
utf8.test \
|
||||
length.test \
|
||||
equals.test \
|
||||
tostring.test \
|
||||
lunabbrev.test \
|
||||
tunabbrev.test \
|
||||
nenoform.test \
|
||||
tunenoform.test \
|
||||
unabbrevwm.test \
|
||||
consterm.test \
|
||||
kind.test \
|
||||
remove_x.test \
|
||||
ltlrel.test \
|
||||
ltlgrind.test \
|
||||
ltlcrossgrind.test \
|
||||
ltlfilt.test \
|
||||
exclusive-ltl.test \
|
||||
latex.test \
|
||||
lbt.test \
|
||||
lenient.test \
|
||||
rand.test \
|
||||
isop.test \
|
||||
syntimpl.test \
|
||||
reduc.test \
|
||||
reduc0.test \
|
||||
reducpsl.test \
|
||||
reduccmp.test \
|
||||
uwrm.test \
|
||||
eventuniv.test \
|
||||
stutter-ltl.test
|
||||
|
||||
TESTS_graph = \
|
||||
graph.test \
|
||||
ngraph.test \
|
||||
tgbagraph.test
|
||||
|
||||
TESTS_kripke = \
|
||||
kripke.test \
|
||||
bad_parsing.test
|
||||
|
||||
TESTS_twa = \
|
||||
acc.test \
|
||||
|
|
|
|||
95
src/tests/bad_parsing.test
Executable file
95
src/tests/bad_parsing.test
Executable file
|
|
@ -0,0 +1,95 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE)
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
cat >input <<\EOF
|
||||
state;
|
||||
EOF
|
||||
|
||||
cat >expected <<\EOF
|
||||
input:1.6: syntax error, unexpected ;, expecting ","
|
||||
EOF
|
||||
|
||||
run 1 ../parse_print input 2> output
|
||||
cat output | grep -v + > res
|
||||
diff expected res
|
||||
|
||||
rm -f output res expected
|
||||
|
||||
cat >input <<\EOF
|
||||
state1, "a & b, state2;
|
||||
EOF
|
||||
|
||||
cat >expected <<\EOF
|
||||
input:1.9-24: unterminated string
|
||||
input:1.25-24: syntax error, unexpected $end, expecting ","
|
||||
EOF
|
||||
|
||||
run 1 ../parse_print input 2> output
|
||||
cat output | grep -v + > res
|
||||
diff expected res
|
||||
|
||||
rm -f output res expected
|
||||
|
||||
|
||||
cat >input <<\EOF
|
||||
state, "", ;
|
||||
,,;
|
||||
EOF
|
||||
|
||||
cat >expected <<\EOF
|
||||
input:1.9-8: empty input
|
||||
input:2.1: syntax error, unexpected ",", expecting $end
|
||||
EOF
|
||||
|
||||
run 1 ../parse_print input 2> output
|
||||
cat output | grep -v + > res
|
||||
diff expected res
|
||||
|
||||
# The diagnostic should be the same with DOS return lines
|
||||
perl -pi -e 's/$/\r/' input
|
||||
run 1 ../parse_print input 2> output
|
||||
cat output | grep -v + > res
|
||||
diff expected res
|
||||
|
||||
|
||||
rm -f output res expected
|
||||
|
||||
cat >input <<\EOF
|
||||
state,, state3
|
||||
state2, "a & b", state2;
|
||||
EOF
|
||||
|
||||
|
||||
s="input:2.7: syntax error, unexpected \",\", expecting STRING"
|
||||
s2=" or UNTERMINATED_STRING or IDENT or ;"
|
||||
string="$s$s2";
|
||||
|
||||
echo $string > expected
|
||||
|
||||
run 1 ../parse_print input 2> output
|
||||
cat output | grep -v + > res
|
||||
diff expected res
|
||||
|
||||
rm -f output res expected
|
||||
33
src/tests/bare.test
Executable file
33
src/tests/bare.test
Executable file
|
|
@ -0,0 +1,33 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
test "`../../bin/ltlfilt -p -f 'GFP_0.b_c'`" = "(G(F(P_0.b_c)))"
|
||||
test "`../../bin/ltlfilt -f 'GFP_0.b_c'`" = "GFP_0.b_c"
|
||||
foo=`../../bin/ltlfilt -p -f 'GF"P_0.b_c"'`
|
||||
test "$foo" = "(G(F(P_0.b_c)))"
|
||||
|
||||
foo=`../../bin/ltlfilt -p -f '"a.b" U c.d.e'`
|
||||
test "$foo" = "(a.b) U (c.d.e)"
|
||||
|
||||
foo=`../../bin/ltlfilt -f '"a.b" U c.d.e'`
|
||||
test "$foo" = "a.b U c.d.e"
|
||||
84
src/tests/consterm.cc
Normal file
84
src/tests/consterm.cc
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et
|
||||
// Dévelopement de l'Epita (LRDE).
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <sstream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
void
|
||||
syntax(char *prog)
|
||||
{
|
||||
std::cerr << prog << " formula" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char **argv)
|
||||
{
|
||||
if (argc != 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
std::ifstream input(argv[1]);
|
||||
if (!input)
|
||||
{
|
||||
std::cerr << "failed to open " << argv[1] << '\n';
|
||||
return 2;
|
||||
}
|
||||
|
||||
std::string s;
|
||||
while (std::getline(input, s))
|
||||
{
|
||||
if (s[0] == '#') // Skip comments
|
||||
{
|
||||
std::cerr << s << '\n';
|
||||
continue;
|
||||
}
|
||||
std::istringstream ss(s);
|
||||
std::string form;
|
||||
bool expected;
|
||||
std::getline(ss, form, ',');
|
||||
ss >> expected;
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* f1 = spot::ltl::parse_sere(form, p1);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, form, p1))
|
||||
return 2;
|
||||
|
||||
bool b = f1->accepts_eword();
|
||||
std::cout << form << ',' << b << '\n';
|
||||
if (b != expected)
|
||||
{
|
||||
std::cerr << "computed '" << b
|
||||
<< "' but expected '" << expected << "'\n";
|
||||
return 2;
|
||||
}
|
||||
f1->destroy();
|
||||
}
|
||||
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::bunop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return 0;
|
||||
}
|
||||
54
src/tests/consterm.test
Executable file
54
src/tests/consterm.test
Executable file
|
|
@ -0,0 +1,54 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2010, 2015 Laboratoire de Recherche et Devéloppement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the constant_term visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >input2 <<EOF
|
||||
1,0
|
||||
0,0
|
||||
[*0],1
|
||||
a*,1
|
||||
0*,1
|
||||
a[*0],1
|
||||
a[*0..],1
|
||||
a[*0..3],1
|
||||
a[*1..3],0
|
||||
a[*3],0
|
||||
a[*..4][*3],1
|
||||
a[*1..4][*3],0
|
||||
a[*1..4][*0..3],1
|
||||
((a ; b) + c),0
|
||||
((a ; b) + [*0]),1
|
||||
((a ; b) + [*0]) & e,0
|
||||
((a ; b) + [*0]) & [*0],1
|
||||
((a ; b) + [*0]) & (a* + b),1
|
||||
# test braces
|
||||
{{a ; b} + {[*0]}} & {a* + b},1
|
||||
(a + [*0]);(b + [*0]);(c + [*0]),1
|
||||
(a + [*0]);(b + e);(c + [*0]),0
|
||||
(a + [*0]);(b + e)*;(c + [*0]),1
|
||||
EOF
|
||||
|
||||
run 0 ../consterm input2
|
||||
|
|
@ -65,6 +65,7 @@ VALGRIND='@VALGRIND@'
|
|||
SPIN='@SPIN@'
|
||||
LTL2BA='@LTL2BA@'
|
||||
PYTHON='@PYTHON@'
|
||||
top_srcdir='../@top_srcdir@'
|
||||
|
||||
# The test cases assume these variable are undefined
|
||||
unset SPOT_DOTEXTRA
|
||||
|
|
|
|||
227
src/tests/equals.test
Executable file
227
src/tests/equals.test
Executable file
|
|
@ -0,0 +1,227 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the equals visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
cat >equal.txt <<\EOF
|
||||
# A few things which are equal
|
||||
a, a
|
||||
~a, !a
|
||||
1, 1
|
||||
0, 0
|
||||
a => b, a --> b
|
||||
a <-> b, a <--> b
|
||||
G a , G a
|
||||
a U b, a U b
|
||||
a & b, a & b
|
||||
a & b, b & a
|
||||
a & b & c, c & a && b
|
||||
a & b & c, b & c & a
|
||||
a && b & a, b & a & b
|
||||
a & b, b & a & b
|
||||
a & b, b & a & a
|
||||
a & b & (c |(f U g)|| e), b & a & a & (c | e |(f U g)| e | c) & b
|
||||
a & a, a
|
||||
a & a & true, a
|
||||
a & false & a, false
|
||||
a | false | a, a
|
||||
true | a | a, true
|
||||
Ga=1*Gb=0, (G(a)) & (G(!b))
|
||||
FFx, Fx
|
||||
FFFFFx, Fx
|
||||
GGx, Gx
|
||||
GGGGGx, Gx
|
||||
!!x, x
|
||||
!!!!!x, !x
|
||||
{[*0];x}<>->1, {x}<>->1
|
||||
{x;[*0]}<>->1, {x}<>-> 1
|
||||
{[*0];x;[*0];[*0]}<>->1, {x}<>->1
|
||||
{[*0];x;[*0];x;[*0]}<>->1, {x;x}<>->1
|
||||
{x;x;x;[*0];x;x}<>->1, {x;x;x;x;x}<>->1
|
||||
{x;0;x;x;x}<>->1, 0
|
||||
{x;0;x;x;x}[]->1, 1
|
||||
{0*;1}<>->x, x
|
||||
{[*0]*;1}<>->x, x
|
||||
{x;x}<>->FF(0), 0
|
||||
{x;x}<>->GX(1), {x;x}<>->1
|
||||
{x;x}[]->GX(1), 1
|
||||
{x;x}[]->FF(0), {x;x}[]->0
|
||||
{x;x}[]->y, {x;x}|->y
|
||||
{x;x}[]->y, {x;x}(y)
|
||||
{a*}!, {a*}<>->1
|
||||
{a -> b} (c), !(a->b)|c
|
||||
{a & !b}!, a & !b
|
||||
{a;[*0]}|->!Xb, !a | !Xb
|
||||
{{a;b}:b:c:d*:e:f}!, {{a;b}:{b && c }:d[*]:{e && f}}!
|
||||
{a:b:c}|->!Xb, !(a&&b&&c) | !Xb
|
||||
{a:b:c*}|->!Xb, {(a&&b):c*}|-> !Xb
|
||||
{a&b&c*}|->!Xb, {(a&&b)&c*}|-> !Xb
|
||||
{[*]&&a&&[*]}!, a
|
||||
{[*]||a||[*]}!, {[*]}!
|
||||
{0&{f;g*}}!, 0
|
||||
{1&{f;g*}}!, {f;g*}!
|
||||
# Precedence
|
||||
a & b ^ c | d, d | c ^ b & a
|
||||
|
||||
# Corner cases parsing
|
||||
FFG__GFF, F(F(G("__GFF")))
|
||||
|
||||
# Trivial simplifications
|
||||
{0*}<>->a, {[*0]}<>->a
|
||||
{[*0]*}<>->a, {[*0]}<>->a
|
||||
{Exp**}<>->a, {Exp*}<>->a
|
||||
FF(Exp), F(Exp)
|
||||
GG(Exp), G(Exp)
|
||||
F(0), 0
|
||||
G(0), 0
|
||||
F(1), 1
|
||||
G(1), 1
|
||||
F({[*0]}<>->1), F({[*0]}<>->1)
|
||||
G({[*0]}<>->1), G({[*0]}<>->1)
|
||||
F({1}<>->1), 1
|
||||
G({1}<>->1), 1
|
||||
!1, 0
|
||||
!0, 1
|
||||
!!Exp, Exp
|
||||
|
||||
(1 => Exp), Exp
|
||||
(0 => Exp), 1
|
||||
(Exp => 1), 1
|
||||
(Exp => 0), !Exp
|
||||
(Exp => Exp), 1
|
||||
(1 ^ Exp), !Exp
|
||||
(0 ^ Exp), Exp
|
||||
(Exp ^ Exp), 0
|
||||
(0 <=> Exp), !Exp
|
||||
(1 <=> Exp), Exp
|
||||
(Exp <=> Exp), 1
|
||||
(Exp U 1), 1
|
||||
(Exp U 0), 0
|
||||
(0 U Exp), Exp
|
||||
(Exp U Exp), Exp
|
||||
(Exp R 1), 1
|
||||
(Exp R 0), 0
|
||||
(Exp R Exp), Exp
|
||||
(1 R Exp), Exp
|
||||
(Exp W 1), 1
|
||||
(0 W Exp), Exp
|
||||
(1 W Exp), 1
|
||||
(Exp W Exp), Exp
|
||||
(Exp M 0), 0
|
||||
(1 M Exp), Exp
|
||||
(0 M Exp), 0
|
||||
(Exp M Exp), Exp
|
||||
|
||||
{1:{a;b}:1:c*}!, {{a;b}:c*}!
|
||||
{c*:1:{a;b}:1}!, {c*:{a;b}}!
|
||||
|
||||
{z;a*;b*;*;c;d;*;b*;e;a*;*;b*}, {z;[*];c;d;[*];e;[*]}
|
||||
{((a;b)|[*0]);[*];c}!, {[*];c}!
|
||||
{a;a;a*;a;b;b[*];c[*2:3];c[*4:5]}, {a[*3..];b[+];c[*6..8]}
|
||||
|
||||
{a[*0]}, {[*0]}
|
||||
{a[*..]}, {a[*]}
|
||||
{a[*2..3][*4..5]}, {a[*8..15]}
|
||||
{a[*4..5][*2..3]}, {a[*4..5][*2..3]}
|
||||
{a[*2:3][*]}, {a[*2 to 3][*]}
|
||||
{a[*1..3][*]}, {a[*]}
|
||||
{a[*][*2..3]}, {a[*]}
|
||||
{a[*..3][*2]}, {a[*..6]}
|
||||
{a[*..3][*to2]}, {a[*:6]}
|
||||
{a[*..3][*2..$]}, {a[*]}
|
||||
{a[*..3][*2:]}, {a[*:inf]}
|
||||
{a[*1..]}, {a[+]}
|
||||
{a[*1]}, {a}
|
||||
{a[+][*1..3]}, {a[+]}
|
||||
{a[*1..3][+]}, {a[+]}
|
||||
{[*2][+]}, {[*2][+]}
|
||||
{[+][*2]}, {[*2..inf]}
|
||||
|
||||
{0[=2]}, 0
|
||||
{0[=2..]}, 0
|
||||
{0[=1..10]}, 0
|
||||
{0[=0]}, {[*]}
|
||||
{0[=0..10]}, {*}
|
||||
{0[=0..]}, {*}
|
||||
{1[=0]}, {[*0]}
|
||||
{1[=1..2]}, {[*1\,2]}
|
||||
{1[=..4]}, {1[*..4]}
|
||||
{b[=0]}, {(!b)[*]}
|
||||
{b[=0to$]}, {*}
|
||||
|
||||
{0[->10..100];b}, 0
|
||||
{0[->1..];b}, 0
|
||||
{0[->0\,100];b}, b
|
||||
{0[->0..$];b}, b
|
||||
!{1[->0];b}, !b
|
||||
{1[->10\,20];b}, {[*10..20];b}
|
||||
{1[->..];b}, {[*1..];b}
|
||||
{{a&!c}[->0];b}, b
|
||||
|
||||
{(a|c)[:*0..3];d}, {1;d}
|
||||
{(a|c)[:*1..3];d}, {(a|c);d}
|
||||
{0[:*0..3];d}, {1;d}
|
||||
{0[:*1..3];d}, 0
|
||||
{1[:*0..3];d}, {1;d}
|
||||
{1[:*1..3];d}, {1;d}
|
||||
{[*0][:*0..3];d}, {1;d}
|
||||
{[*0][:*1..3];d}, 0
|
||||
{(a*;b|c)[:*1to3][:*2:4]}, {(a*;b|c)[:*2..12]}
|
||||
{(a*;b|c)[:*][:+]}, {(a*;b|c)[:*]}
|
||||
{(a*;b|c)[:*0]}, 1
|
||||
{(a*;b|c)[:*1]}, {(a*;b|c)}
|
||||
{(a;b):(a;b):(a;b)[:*2]:(a;b):b*:b*:(c;d)[:*1]}, {(a;b)[:*5]:b*[:*2]:(c;d)}
|
||||
EOF
|
||||
|
||||
|
||||
cat >nequal.txt <<\EOF
|
||||
# other formulae which are not
|
||||
a, b
|
||||
1, 0
|
||||
a => b, b => a
|
||||
a => b, a <=> b
|
||||
a => b, a U b
|
||||
a R b, a U b
|
||||
a & b & c, c & a
|
||||
b & c, c & a & b
|
||||
a & b & (c |(f U g)| e), b & a & a & (c | e |(g U g)| e | c) & b
|
||||
{a*}, {a*}<>->1
|
||||
!{a*}, {a*}<>->1
|
||||
{a*}, {a*}!
|
||||
!{a*}, {a*}!
|
||||
|
||||
# 1 should not be removed in the following two formulae
|
||||
{1&{g*}}!, {g*}!
|
||||
{1|{b;c}}<>->a, {b;c}<>->a
|
||||
# make sure twin arguments are not reduced in Fusion.
|
||||
{(a;!a)*:(a;!a)*:b}!, {(a;!a)*:b}!
|
||||
# make sure 1:a* is not reduced to a*.
|
||||
{(1:a*);b}!, {a*;b}!
|
||||
EOF
|
||||
|
||||
run 0 ../equals equal.txt
|
||||
run 0 ../nequals nequal.txt
|
||||
268
src/tests/equalsf.cc
Normal file
268
src/tests/equalsf.cc
Normal file
|
|
@ -0,0 +1,268 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <sstream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/lunabbrev.hh"
|
||||
#include "ltlvisit/tunabbrev.hh"
|
||||
#include "ltlvisit/dump.hh"
|
||||
#include "ltlvisit/wmunabbrev.hh"
|
||||
#include "ltlvisit/nenoform.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlvisit/simplify.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " [-E] file" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
bool check_first = true;
|
||||
|
||||
if (argc > 1 && !strcmp(argv[1], "-E"))
|
||||
{
|
||||
check_first = false;
|
||||
argv[1] = argv[0];
|
||||
++argv;
|
||||
--argc;
|
||||
}
|
||||
if (argc != 2)
|
||||
syntax(argv[0]);
|
||||
std::ifstream input(argv[1]);
|
||||
if (!input)
|
||||
{
|
||||
std::cerr << "failed to open " << argv[1] << '\n';
|
||||
return 2;
|
||||
}
|
||||
|
||||
std::string s;
|
||||
unsigned line = 0;
|
||||
while (std::getline(input, s))
|
||||
{
|
||||
++line;
|
||||
std::cerr << line << ": " << s << '\n';
|
||||
if (s[0] == '#') // Skip comments
|
||||
continue;
|
||||
std::vector<std::string> formulas;
|
||||
{
|
||||
std::istringstream ss(s);
|
||||
std::string form;
|
||||
while (std::getline(ss, form, ','))
|
||||
{
|
||||
std::string tmp;
|
||||
while (form.size() > 0 && form.back() == '\\'
|
||||
&& std::getline(ss, tmp, ','))
|
||||
{
|
||||
form.back() = ',';
|
||||
form += tmp;
|
||||
}
|
||||
formulas.push_back(form);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned size = formulas.size();
|
||||
if (size == 0) // Skip empty lines
|
||||
continue;
|
||||
|
||||
if (size == 1)
|
||||
{
|
||||
std::cerr << "Not enough formulas on line " << line << '\n';
|
||||
return 2;
|
||||
}
|
||||
|
||||
spot::ltl::parse_error_list p2;
|
||||
const spot::ltl::formula* f2 = spot::ltl::parse(formulas[size - 1], p2);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, formulas[size - 1], p2))
|
||||
return 2;
|
||||
|
||||
for (unsigned n = 0; n < size - 1; ++n)
|
||||
{
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* f1 = spot::ltl::parse(formulas[n], p1);
|
||||
|
||||
if (check_first &&
|
||||
spot::ltl::format_parse_errors(std::cerr, formulas[n], p1))
|
||||
return 2;
|
||||
|
||||
int exit_code = 0;
|
||||
|
||||
{
|
||||
#if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
|
||||
const spot::ltl::formula* tmp;
|
||||
#endif
|
||||
#ifdef LUNABBREV
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::unabbreviate_logic(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef TUNABBREV
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::unabbreviate_ltl(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef WM
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::unabbreviate_wm(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef NENOFORM
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::negative_normal_form(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef REDUC
|
||||
spot::ltl::ltl_simplifier_options opt(true, true, true,
|
||||
false, false);
|
||||
# ifdef EVENT_UNIV
|
||||
opt.favor_event_univ = true;
|
||||
# endif
|
||||
spot::ltl::ltl_simplifier simp(opt);
|
||||
{
|
||||
const spot::ltl::formula* tmp;
|
||||
tmp = f1;
|
||||
f1 = simp.simplify(f1);
|
||||
|
||||
if (!simp.are_equivalent(f1, tmp))
|
||||
{
|
||||
std::cerr
|
||||
<< "Source and simplified formulae are not equivalent!\n";
|
||||
std::cerr
|
||||
<< "Simplified: " << spot::ltl::to_string(f1) << '\n';
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
tmp->destroy();
|
||||
}
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef REDUC_TAU
|
||||
spot::ltl::ltl_simplifier_options opt(false, false, false,
|
||||
true, false);
|
||||
spot::ltl::ltl_simplifier simp(opt);
|
||||
{
|
||||
const spot::ltl::formula* tmp;
|
||||
tmp = f1;
|
||||
f1 = simp.simplify(f1);
|
||||
|
||||
if (!simp.are_equivalent(f1, tmp))
|
||||
{
|
||||
std::cerr
|
||||
<< "Source and simplified formulae are not equivalent!\n";
|
||||
std::cerr
|
||||
<< "Simplified: " << spot::ltl::to_string(f1) << '\n';
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
tmp->destroy();
|
||||
}
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef REDUC_TAUSTR
|
||||
spot::ltl::ltl_simplifier_options opt(false, false, false,
|
||||
true, true);
|
||||
spot::ltl::ltl_simplifier simp(opt);
|
||||
{
|
||||
const spot::ltl::formula* tmp;
|
||||
tmp = f1;
|
||||
f1 = simp.simplify(f1);
|
||||
|
||||
if (!simp.are_equivalent(f1, tmp))
|
||||
{
|
||||
std::cerr
|
||||
<< "Source and simplified formulae are not equivalent!\n";
|
||||
std::cerr
|
||||
<< "Simplified: " << spot::ltl::to_string(f1) << '\n';
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
tmp->destroy();
|
||||
}
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
|
||||
exit_code |= f1 != f2;
|
||||
|
||||
#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
|
||||
spot::ltl::ltl_simplifier simp;
|
||||
#endif
|
||||
|
||||
if (!simp.are_equivalent(f1, f2))
|
||||
{
|
||||
#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
|
||||
std::cerr
|
||||
<< "Source and destination formulae are not equivalent!\n";
|
||||
#else
|
||||
std::cerr
|
||||
<< "Simpl. and destination formulae are not equivalent!\n";
|
||||
#endif
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
#if NEGATE
|
||||
exit_code ^= 1;
|
||||
#endif
|
||||
if (exit_code)
|
||||
{
|
||||
spot::ltl::dump(std::cerr, f1) << std::endl;
|
||||
spot::ltl::dump(std::cerr, f2) << std::endl;
|
||||
return exit_code;
|
||||
}
|
||||
|
||||
}
|
||||
f1->destroy();
|
||||
}
|
||||
f2->destroy();
|
||||
}
|
||||
|
||||
spot::ltl::atomic_prop::dump_instances(std::cerr);
|
||||
spot::ltl::unop::dump_instances(std::cerr);
|
||||
spot::ltl::binop::dump_instances(std::cerr);
|
||||
spot::ltl::multop::dump_instances(std::cerr);
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return 0;
|
||||
}
|
||||
64
src/tests/eventuniv.test
Executable file
64
src/tests/eventuniv.test
Executable file
|
|
@ -0,0 +1,64 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
|
||||
# Developpement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
cat >reduceu.txt <<EOF
|
||||
Xa | GFb, Xa | GFb
|
||||
X(a | GXFb), Xa | GFb
|
||||
Xa & GFb, Xa & GFb
|
||||
X(a & GXFb), Xa & GFb
|
||||
|
||||
F(a & b & GFc & FGd), F(a & b) & G(Fc & FGd)
|
||||
Fa | Fb | GFc | GFd, F(a|b) | GF(c | d)
|
||||
Fa | Fb | GFc | GFd | FGe, F(a|b) | F(G(e) | GF(c | d))
|
||||
Ga | Gb | GFd | FGe | FGf, Ga | Gb | F(GFd | Ge | Gf)
|
||||
|
||||
G(Ga & Fb & c & GFd), G(a&c) & G(Fb & Fd)
|
||||
G(Ga & GFb & c & GFd), G(a&c) & G(Fb & Fd)
|
||||
G(a & GFb & c & GFd), G(a&c) & G(Fb & Fd)
|
||||
G(Ga & Fb & c & GFd & FGe), G(a & c) & G(Fb & Fd & FGe)
|
||||
G(Ga & XFGb & c & FGd & FGe), FG(b & d & e) & G(a & c)
|
||||
G(Ga & GXFb & c & FGd & FGe & Fc), G(Fb & FG(d & e)) & G(a & c)
|
||||
Ga & Gb & GFd & FGe & FGf, G(Fd & FG(e & f)) & G(a & b)
|
||||
G(Ga & Gb & GFd & FGe) & FGf, G(Fd & FG(e & f)) & G(a & b)
|
||||
|
||||
a U (b | Fc), (a U b) | Fc
|
||||
a W (b | Fc), (a W b) | Fc
|
||||
a U (b & GFc), (a U b) & GFc
|
||||
# Unchanged
|
||||
a W (b & GFc), a W (b & GFc)
|
||||
# Unchanged
|
||||
(a | Gc) W g, (a | Gc) W g
|
||||
# Unchanged
|
||||
(a | Gc) U g, (a | Gc) U g
|
||||
(a & GFc) M b, (a M b) & GFc
|
||||
# Unchanged
|
||||
(a | GFc) M b, (a | GFc) M b
|
||||
# Unchanged
|
||||
(a & GFc) R b, (a & GFc) R b
|
||||
# Unchanged
|
||||
(a | GFc) R b, (a | GFc) R b
|
||||
a R (b & Gc), (a R b) & Gc
|
||||
a M (b & Gc), (a M b) & Gc
|
||||
EOF
|
||||
|
||||
run 0 ../reduceu reduceu.txt
|
||||
56
src/tests/exclusive-ltl.test
Executable file
56
src/tests/exclusive-ltl.test
Executable file
|
|
@ -0,0 +1,56 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2015 Laboratoire de Recherche et Développement de
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >formulas <<EOF
|
||||
GFa
|
||||
a U b
|
||||
a U b U c
|
||||
a U b U d U e
|
||||
a U b U c U d U e
|
||||
EOF
|
||||
|
||||
cat >expected <<EOF
|
||||
GFa
|
||||
(a U b) & G!(a & b)
|
||||
(a U (b U c)) & G(!(a & b) & !(a & c) & !(b & c))
|
||||
(a U (b U (d U e))) & G(!(a & b) & !(d & e))
|
||||
(a U (b U (c U (d U e)))) & G(!(a & b) & !(a & c) & !(b & c) & !(d & e))
|
||||
EOF
|
||||
|
||||
run 0 ../../bin/ltlfilt --exclusive-ap=a,b,c --exclusive-ap=d,e formulas >out
|
||||
cat out
|
||||
diff out expected
|
||||
|
||||
run 0 ../../bin/ltlfilt --exclusive-ap='"a" ,b, "c" ' --exclusive-ap=' d , e' \
|
||||
formulas >out
|
||||
cat out
|
||||
diff out expected
|
||||
|
||||
../../bin/ltlfilt --exclusive-ap='"a","b' 2>stderr && exit 1
|
||||
grep 'missing closing ."' stderr
|
||||
../../bin/ltlfilt --exclusive-ap='a,,b' 2>stderr && exit 1
|
||||
grep "unexpected ',' in a,,b" stderr
|
||||
../../bin/ltlfilt --exclusive-ap='"a"b' 2>stderr && exit 1
|
||||
grep "unexpected character 'b' in \"a\"b" stderr
|
||||
312
src/tests/graph.cc
Normal file
312
src/tests/graph.cc
Normal file
|
|
@ -0,0 +1,312 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
#include <iostream>
|
||||
#include "graph/graph.hh"
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, spot::digraph<SL, TL>& g, unsigned n)
|
||||
{
|
||||
out << " [label=\"" << g.state_data(n) << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, spot::digraph<void, TL>&, unsigned)
|
||||
{
|
||||
out << '\n';
|
||||
}
|
||||
|
||||
template <typename SL, typename TL, typename TR>
|
||||
void
|
||||
dot_trans(std::ostream& out, spot::digraph<SL, TL>&, TR& tr)
|
||||
{
|
||||
out << " [label=\"" << tr.data() << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename SL, typename TR>
|
||||
void
|
||||
dot_trans(std::ostream& out, spot::digraph<SL, void>&, TR&)
|
||||
{
|
||||
out << '\n';
|
||||
}
|
||||
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot(std::ostream& out, spot::digraph<SL, TL>& g)
|
||||
{
|
||||
out << "digraph {\n";
|
||||
unsigned c = g.num_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
dot_state(out, g, s);
|
||||
for (auto& t: g.out(s))
|
||||
{
|
||||
out << ' ' << s << " -> " << t.dst;
|
||||
dot_trans(out, g, t);
|
||||
}
|
||||
}
|
||||
out << "}\n";
|
||||
}
|
||||
|
||||
|
||||
bool g1(const spot::digraph<void, void>& g,
|
||||
unsigned s, int e)
|
||||
{
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s))
|
||||
{
|
||||
(void) t;
|
||||
++f;
|
||||
}
|
||||
return f == e;
|
||||
}
|
||||
|
||||
bool f1()
|
||||
{
|
||||
spot::digraph<void, void> g(3);
|
||||
|
||||
auto s1 = g.new_state();
|
||||
auto s2 = g.new_state();
|
||||
auto s3 = g.new_state();
|
||||
g.new_transition(s1, s2);
|
||||
g.new_transition(s1, s3);
|
||||
g.new_transition(s2, s3);
|
||||
g.new_transition(s3, s1);
|
||||
g.new_transition(s3, s2);
|
||||
g.new_transition(s3, s3);
|
||||
|
||||
dot(std::cout, g);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
(void) t;
|
||||
++f;
|
||||
}
|
||||
return f == 2
|
||||
&& g1(g, s3, 3)
|
||||
&& g1(g, s2, 1)
|
||||
&& g1(g, s1, 2);
|
||||
}
|
||||
|
||||
|
||||
bool f2()
|
||||
{
|
||||
spot::digraph<int, void> g(3);
|
||||
|
||||
auto s1 = g.new_state(1);
|
||||
auto s2 = g.new_state(2);
|
||||
auto s3 = g.new_state(3);
|
||||
g.new_transition(s1, s2);
|
||||
g.new_transition(s1, s3);
|
||||
g.new_transition(s2, s3);
|
||||
g.new_transition(s3, s2);
|
||||
|
||||
dot(std::cout, g);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += g.state_data(t.dst);
|
||||
}
|
||||
return f == 5;
|
||||
}
|
||||
|
||||
bool f3()
|
||||
{
|
||||
spot::digraph<void, int> g(3);
|
||||
|
||||
auto s1 = g.new_state();
|
||||
auto s2 = g.new_state();
|
||||
auto s3 = g.new_state();
|
||||
g.new_transition(s1, s2, 1);
|
||||
g.new_transition(s1, s3, 2);
|
||||
g.new_transition(s2, s3, 3);
|
||||
g.new_transition(s3, s2, 4);
|
||||
|
||||
dot(std::cout, g);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.label;
|
||||
}
|
||||
return f == 3 && g.states().size() == 3;
|
||||
}
|
||||
|
||||
bool f4()
|
||||
{
|
||||
spot::digraph<int, int> g(3);
|
||||
|
||||
auto s1 = g.new_state(2);
|
||||
auto s2 = g.new_state(3);
|
||||
auto s3 = g.new_state(4);
|
||||
g.new_transition(s1, s2, 1);
|
||||
g.new_transition(s1, s3, 2);
|
||||
g.new_transition(s2, s3, 3);
|
||||
g.new_transition(s3, s2, 4);
|
||||
|
||||
dot(std::cout, g);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.label * g.state_data(t.dst);
|
||||
}
|
||||
return f == 11;
|
||||
}
|
||||
|
||||
bool f5()
|
||||
{
|
||||
spot::digraph<void, std::pair<int, float>> g(3);
|
||||
|
||||
auto s1 = g.new_state();
|
||||
auto s2 = g.new_state();
|
||||
auto s3 = g.new_state();
|
||||
g.new_transition(s1, s2, std::make_pair(1, 1.2f));
|
||||
g.new_transition(s1, s3, std::make_pair(2, 1.3f));
|
||||
g.new_transition(s2, s3, std::make_pair(3, 1.4f));
|
||||
g.new_transition(s3, s2, std::make_pair(4, 1.5f));
|
||||
|
||||
int f = 0;
|
||||
float h = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += std::get<0>(t);
|
||||
h += std::get<1>(t);
|
||||
}
|
||||
return f == 3 && (h > 2.49 && h < 2.51);
|
||||
}
|
||||
|
||||
bool f6()
|
||||
{
|
||||
spot::digraph<void, std::pair<int, float>> g(3);
|
||||
|
||||
auto s1 = g.new_state();
|
||||
auto s2 = g.new_state();
|
||||
auto s3 = g.new_state();
|
||||
g.new_transition(s1, s2, 1, 1.2f);
|
||||
g.new_transition(s1, s3, 2, 1.3f);
|
||||
g.new_transition(s2, s3, 3, 1.4f);
|
||||
g.new_transition(s3, s2, 4, 1.5f);
|
||||
|
||||
int f = 0;
|
||||
float h = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.first;
|
||||
h += t.second;
|
||||
}
|
||||
return f == 3 && (h > 2.49 && h < 2.51);
|
||||
}
|
||||
|
||||
bool f7()
|
||||
{
|
||||
spot::digraph<int, int, true> g(3);
|
||||
auto s1 = g.new_state(2);
|
||||
auto s2 = g.new_state(3);
|
||||
auto s3 = g.new_state(4);
|
||||
g.new_transition(s1, {s2, s3}, 1);
|
||||
g.new_transition(s1, {s3}, 2);
|
||||
g.new_transition(s2, {s3}, 3);
|
||||
g.new_transition(s3, {s2}, 4);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
for (auto& tt: t.dst)
|
||||
{
|
||||
f += t.label * g.state_data(tt);
|
||||
}
|
||||
}
|
||||
return f == 15;
|
||||
}
|
||||
|
||||
|
||||
struct int_pair
|
||||
{
|
||||
int one;
|
||||
int two;
|
||||
|
||||
friend std::ostream& operator<<(std::ostream& os, int_pair p)
|
||||
{
|
||||
os << '(' << p.one << ',' << p.two << ')';
|
||||
return os;
|
||||
}
|
||||
|
||||
#if __GNUC__ <= 4 && __GNUC_MINOR__ <= 6
|
||||
int_pair(int one, int two)
|
||||
: one(one), two(two)
|
||||
{
|
||||
}
|
||||
|
||||
int_pair()
|
||||
{
|
||||
}
|
||||
#endif
|
||||
};
|
||||
|
||||
bool f8()
|
||||
{
|
||||
spot::digraph<int_pair, int_pair> g(3);
|
||||
auto s1 = g.new_state(2, 4);
|
||||
auto s2 = g.new_state(3, 6);
|
||||
auto s3 = g.new_state(4, 8);
|
||||
g.new_transition(s1, s2, 1, 3);
|
||||
g.new_transition(s1, s3, 2, 5);
|
||||
g.new_transition(s2, s3, 3, 7);
|
||||
g.new_transition(s3, s2, 4, 9);
|
||||
|
||||
dot(std::cout, g);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.one * g.state_data(t.dst).one;
|
||||
f += t.two * g.state_data(t.dst).two;
|
||||
}
|
||||
return f == 69;
|
||||
}
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
bool a1 = f1();
|
||||
bool a2 = f2();
|
||||
bool a3 = f3();
|
||||
bool a4 = f4();
|
||||
bool a5 = f5();
|
||||
bool a6 = f6();
|
||||
bool a7 = f7();
|
||||
bool a8 = f8();
|
||||
std::cout << a1 << ' '
|
||||
<< a2 << ' '
|
||||
<< a3 << ' '
|
||||
<< a4 << ' '
|
||||
<< a5 << ' '
|
||||
<< a6 << ' '
|
||||
<< a7 << ' '
|
||||
<< a8 << '\n';
|
||||
return !(a1 && a2 && a3 && a4 && a5 && a6 && a7 && a8);
|
||||
}
|
||||
87
src/tests/graph.test
Executable file
87
src/tests/graph.test
Executable file
|
|
@ -0,0 +1,87 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
# While running some benchmark, Tomáš Babiak found that Spot took too
|
||||
# much time (i.e. >1h) to translate those six formulae. It turns out
|
||||
# that the WDBA minimization was performed after the degeneralization
|
||||
# algorithm, while this is not necessary (WDBA will produce a BA, so
|
||||
# we may as well skip degeneralization). Translating these formulae
|
||||
# in the test-suite ensure that they don't take too much time (the
|
||||
# buildfarm will timeout if it does).
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../graph > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph {
|
||||
0
|
||||
0 -> 1
|
||||
0 -> 2
|
||||
1
|
||||
1 -> 2
|
||||
2
|
||||
2 -> 0
|
||||
2 -> 1
|
||||
2 -> 2
|
||||
}
|
||||
digraph {
|
||||
0 [label="1"]
|
||||
0 -> 1
|
||||
0 -> 2
|
||||
1 [label="2"]
|
||||
1 -> 2
|
||||
2 [label="3"]
|
||||
2 -> 1
|
||||
}
|
||||
digraph {
|
||||
0
|
||||
0 -> 1 [label="1"]
|
||||
0 -> 2 [label="2"]
|
||||
1
|
||||
1 -> 2 [label="3"]
|
||||
2
|
||||
2 -> 1 [label="4"]
|
||||
}
|
||||
digraph {
|
||||
0 [label="2"]
|
||||
0 -> 1 [label="1"]
|
||||
0 -> 2 [label="2"]
|
||||
1 [label="3"]
|
||||
1 -> 2 [label="3"]
|
||||
2 [label="4"]
|
||||
2 -> 1 [label="4"]
|
||||
}
|
||||
digraph {
|
||||
0 [label="(2,4)"]
|
||||
0 -> 1 [label="(1,3)"]
|
||||
0 -> 2 [label="(2,5)"]
|
||||
1 [label="(3,6)"]
|
||||
1 -> 2 [label="(3,7)"]
|
||||
2 [label="(4,8)"]
|
||||
2 -> 1 [label="(4,9)"]
|
||||
}
|
||||
1 1 1 1 1 1 1 1
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
|
||||
55
src/tests/isop.test
Executable file
55
src/tests/isop.test
Executable file
|
|
@ -0,0 +1,55 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
cat >input<<EOF
|
||||
(a -> b) & (b -> d)
|
||||
(a -> b) & Xc & (b -> d)
|
||||
GF((a | b) & (b | d))
|
||||
{((a -> b) & (b -> d))*;a*}<>->((a | b) & (!b | !a))
|
||||
EOF
|
||||
|
||||
# Make sure --boolean-to-isop works as expected...
|
||||
run 0 ../../bin/ltlfilt --boolean-to-isop input > output
|
||||
|
||||
cat> expected<<EOF
|
||||
(!a & !b) | (b & d)
|
||||
(!a | b) & (!b | d) & Xc
|
||||
GF(b | (a & d))
|
||||
{{{{!a && !b} | {b && d}}}[*];a[*]}<>-> ((!a & b) | (a & !b))
|
||||
EOF
|
||||
|
||||
cat output
|
||||
diff output expected
|
||||
|
||||
# Make sure it would not give the same output without the option...
|
||||
run 0 ../../bin/ltlfilt input > output
|
||||
|
||||
cat> expected<<EOF
|
||||
(a -> b) & (b -> d)
|
||||
(a -> b) & (b -> d) & Xc
|
||||
GF((a | b) & (b | d))
|
||||
{{{{a -> b} && {b -> d}}}[*];a[*]}<>-> ((a | b) & (!a | !b))
|
||||
EOF
|
||||
|
||||
cat output
|
||||
diff output expected
|
||||
84
src/tests/kind.cc
Normal file
84
src/tests/kind.cc
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2012, 2015 Laboratoire de Recherche et
|
||||
// Developement de l'Epita (LRDE).
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <sstream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
void
|
||||
syntax(char *prog)
|
||||
{
|
||||
std::cerr << prog << " formula" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char **argv)
|
||||
{
|
||||
if (argc != 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
std::ifstream input(argv[1]);
|
||||
if (!input)
|
||||
{
|
||||
std::cerr << "failed to open " << argv[1] << '\n';
|
||||
return 2;
|
||||
}
|
||||
|
||||
std::string s;
|
||||
while (std::getline(input, s))
|
||||
{
|
||||
if (s[0] == '#') // Skip comments
|
||||
{
|
||||
std::cerr << s << '\n';
|
||||
continue;
|
||||
}
|
||||
std::istringstream ss(s);
|
||||
std::string form;
|
||||
std::string expected;
|
||||
std::getline(ss, form, ',');
|
||||
std::getline(ss, expected);
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* f1 = spot::ltl::parse(form, p1);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, form, p1))
|
||||
return 2;
|
||||
|
||||
std::ostringstream so;
|
||||
spot::ltl::print_formula_props(so, f1, true);
|
||||
auto sost = so.str();
|
||||
std::cout << form << ',' << sost << '\n';
|
||||
if (sost != expected)
|
||||
{
|
||||
std::cerr << "computed '" << sost
|
||||
<< "' but expected '" << expected << "'\n";
|
||||
return 2;
|
||||
}
|
||||
f1->destroy();
|
||||
}
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return 0;
|
||||
}
|
||||
135
src/tests/kind.test
Executable file
135
src/tests/kind.test
Executable file
|
|
@ -0,0 +1,135 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the constant_term visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >input<<EOF
|
||||
a,B&!xfLEPSFsgopra
|
||||
a<->b,BxfLEPSFsgopra
|
||||
!a,B&!xfLEPSFsgopra
|
||||
!(a|b),B&xfLEPSFsgopra
|
||||
F(a),&!xLPegopra
|
||||
G(a),&!xLPusopra
|
||||
a U b,&!xfLPgopra
|
||||
a U Fb,&!xLPegopra
|
||||
Ga U b,&!xLPopra
|
||||
1 U a,&!xfLPegopra
|
||||
a W b,&!xfLPsopra
|
||||
a W 0,&!xfLPusopra
|
||||
a M b,&!xfLPgopra
|
||||
a M 1,&!xfLPegopra
|
||||
a R b,&!xfLPsopra
|
||||
0 R b,&!xfLPusopra
|
||||
a R (b R (c R d)),&!xfLPsopra
|
||||
a U (b U (c U d)),&!xfLPgopra
|
||||
a W (b W (c W d)),&!xfLPsopra
|
||||
a M (b M (c M d)),&!xfLPgopra
|
||||
Fa -> Fb,xLPopra
|
||||
Ga -> Fb,xLPgopra
|
||||
Fa -> Gb,xLPsopra
|
||||
(Ga|Fc) -> Fb,xLPopra
|
||||
(Ga|Fa) -> Gb,xLPopra
|
||||
{a;c*;b}|->!Xb,&fPsopra
|
||||
{a;c*;b}|->X!b,&!fPsopra
|
||||
{a;c*;b}|->!Fb,&Psopra
|
||||
{a;c*;b}|->G!b,&!Psopra
|
||||
{a;c*;b}|->!Gb,&Pra
|
||||
{a;c*;b}|->F!b,&!Pra
|
||||
{a;c*;b}|->GFa,&!Pra
|
||||
{a;c*;b}|->FGa,&!Pa
|
||||
{a[+];c[+];b*}|->!Fb,&xPsopra
|
||||
{a[+];c*;b[+]}|->G!b,&!xPsopra
|
||||
{a*;c[+];b[+]}|->!Gb,&xPra
|
||||
{a[+];c*;b[+]}|->F!b,&!xPra
|
||||
{a[+];c[+];b*}|->GFa,&!xPra
|
||||
{a*;c[+];b[+]}|->FGa,&!xPa
|
||||
{a;c;b|(d;e)}|->!Xb,&fPFsgopra
|
||||
{a;c;b|(d;e)}|->X!b,&!fPFsgopra
|
||||
{a;c;b|(d;e)}|->!Fb,&Psopra
|
||||
{a;c;b|(d;e)}|->G!b,&!Psopra
|
||||
{a;c;b|(d;e)}|->!Gb,&Pgopra
|
||||
{a;c;b|(d;e)}|->F!b,&!Pgopra
|
||||
{a;c;b|(d;e)}|->GFa,&!Pra
|
||||
{a;c;b|(d;e)}|->FGa,&!Ppa
|
||||
{a[+] && c[+]}|->!Xb,&fPsopra
|
||||
{a[+] && c[+]}|->X!b,&!fPsopra
|
||||
{a[+] && c[+]}|->!Fb,&xPsopra
|
||||
{a[+] && c[+]}|->G!b,&!xPsopra
|
||||
{a[+] && c[+]}|->!Gb,&xPra
|
||||
{a[+] && c[+]}|->F!b,&!xPra
|
||||
{a[+] && c[+]}|->GFa,&!xPra
|
||||
{a[+] && c[+]}|->FGa,&!xPa
|
||||
{a;c*;b}<>->!Gb,&Pgopra
|
||||
{a;c*;b}<>->F!b,&!Pgopra
|
||||
{a;c*;b}<>->FGb,&!Ppa
|
||||
{a;c*;b}<>->!GFb,&Ppa
|
||||
{a;c*;b}<>->GFb,&!Pa
|
||||
{a;c*;b}<>->!FGb,&Pa
|
||||
{a*;c[+];b[+]}<>->!FGb,&xPa
|
||||
{a;c|d;b}<>->!Gb,&Pgopra
|
||||
{a;c|d;b}<>->G!b,&!Psopra
|
||||
{a;c|d;b}<>->FGb,&!Ppa
|
||||
{a;c|d;b}<>->!GFb,&Ppa
|
||||
{a;c|d;b}<>->GFb,&!Pra
|
||||
{a;c|d;_b}<>->!FGb,&Pr
|
||||
# Equivalent to a&b&c&d
|
||||
{a:b:c:d}!,B&!xfLEPSFsgopra
|
||||
a&b&c&d,B&!xfLEPSFsgopra
|
||||
(Xa <-> XXXc) U (b & Fe),LPgopra
|
||||
(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopra
|
||||
(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopra
|
||||
(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopra
|
||||
(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopra
|
||||
(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPpa
|
||||
(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPra
|
||||
(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPpa
|
||||
(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b)),LPupa
|
||||
(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPra
|
||||
(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b)),LPera
|
||||
(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPepa
|
||||
(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb)),LPa
|
||||
(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPura
|
||||
(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb)),LPa
|
||||
GFa M GFb,&!xLPeua
|
||||
FGa M FGb,&!xLPeupa
|
||||
Fa M GFb,&!xLPera
|
||||
GFa W GFb,&!xLPeura
|
||||
FGa W FGb,&!xLPeua
|
||||
Ga W FGb,&!xLPupa
|
||||
Ga W b,&!xLPsopra
|
||||
Fa M b,&!xLPgopra
|
||||
{a;b*;c},&!fPsopra
|
||||
{a;b*;c}!,&!fPgopra
|
||||
# The negative normal form is {a;b*;c}[]->1
|
||||
!{a;b*;c}!,&fPsopra
|
||||
{a;b*;p112}[]->0,&!fPsopra
|
||||
!{a;b*;c.2},&!fPgopr
|
||||
!{a[+];b*;c[+]},&!xfPgopra
|
||||
{a[+];b*;c[+]},&!xfPsopra
|
||||
{a[+] && b || c[+]},&!fPsopra
|
||||
{a[+] && b[+] || c[+]},&!xfPsopra
|
||||
EOF
|
||||
|
||||
run 0 ../kind input
|
||||
72
src/tests/kripke.test
Executable file
72
src/tests/kripke.test
Executable file
|
|
@ -0,0 +1,72 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2012, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE)
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
run2()
|
||||
{
|
||||
run 0 ../parse_print "$1" > "$1.out"
|
||||
run 0 ../parse_print "$1.out" > "$1.out2"
|
||||
cmp "$1.out" "$1.out2"
|
||||
}
|
||||
|
||||
cat >input1 <<EOF
|
||||
state1, "!b", state2;
|
||||
state2, "a&b", state3;
|
||||
state3, "a", state4 state1;
|
||||
state4, "b", state1;
|
||||
EOF
|
||||
|
||||
run2 input1
|
||||
|
||||
cat >input2 <<EOF
|
||||
state1, , state1 state2;
|
||||
state2, , state1 state2;
|
||||
EOF
|
||||
|
||||
run2 input2
|
||||
|
||||
cat >input3 <<EOF
|
||||
state42, "!b & !a", state40;
|
||||
state40, "!a | b", state42;
|
||||
EOF
|
||||
|
||||
run2 input3
|
||||
|
||||
cat >input4 <<EOF
|
||||
state1, "a&b", state1;
|
||||
EOF
|
||||
|
||||
run2 input4
|
||||
|
||||
cat >input5 <<EOF
|
||||
state51,,state60 state17 state3 state18 state62;
|
||||
EOF
|
||||
|
||||
run2 input5
|
||||
|
||||
cat >input6 <<EOF
|
||||
s42, "a&b|c&d", s51 s69 s73 s7;
|
||||
s7, "a&a&a&!a", s42 s51 s69 s73 s42;
|
||||
EOF
|
||||
|
||||
run2 input6
|
||||
64
src/tests/latex.test
Executable file
64
src/tests/latex.test
Executable file
|
|
@ -0,0 +1,64 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
# Skip this test if we don't find a sufficiently complete LaTeX
|
||||
# installation
|
||||
|
||||
(latexmk --version) || exit 77
|
||||
(pdflatex --version) || exit 77
|
||||
(kpsewhich txfonts.sty) || exit 77
|
||||
(kpsewhich amsmath.sty) || exit 77
|
||||
|
||||
cat >input <<EOF
|
||||
XGFa <-> FGX(!b & !c) | (b ^ a)
|
||||
a U b W c R (d & e) M f
|
||||
{a;b[=2];((c:d*) && f*);e[*2..]}<>-> {((a | [*0])*;b[+]) & (c1[->2])}[]-> h
|
||||
{a;b;c} []=> {d*;e} <>=> !f
|
||||
!{a;b*;c}! -> d
|
||||
{a*;(b;c)[:*3..4];(c;d)[:+];d}!
|
||||
G(uglyname->Fuglierlongname42)
|
||||
EOF
|
||||
|
||||
(
|
||||
cat <<\EOF
|
||||
\documentclass{article}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{spotltl}
|
||||
\begin{document}
|
||||
\begin{tabular}{ll}
|
||||
EOF
|
||||
( ../../bin/ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\';
|
||||
../../bin/genltl --go-theta=1..3 --latex \
|
||||
--format='\texttt{--%F:%L} & $%f$ \\')
|
||||
cat <<\EOF
|
||||
\end{tabular}
|
||||
\end{document}
|
||||
EOF
|
||||
) > output.tex
|
||||
|
||||
TEXINPUTS=$top_srcdir/doc/tl: \
|
||||
latexmk -f -silent -pdf -ps- -dvi- -pvc- output.tex
|
||||
|
||||
# latexmk will have a non-zero exit status on failure, so we will
|
||||
# detect that. However the file output.pdf really ought to be
|
||||
# controled by eye...
|
||||
111
src/tests/lbt.test
Executable file
111
src/tests/lbt.test
Executable file
|
|
@ -0,0 +1,111 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
ltlfilt=../../bin/ltlfilt
|
||||
randltl=../../bin/randltl
|
||||
genltl=../../bin/genltl
|
||||
|
||||
# Some example formulas taken from Ruediger Ehlers's dbaminimizer
|
||||
# http://react.cs.uni-saarland.de/tools/dbaminimizer
|
||||
# which are expected to be processed by ltl2dstar.
|
||||
cat >formulas <<'EOF'
|
||||
& G F a G F b
|
||||
X X a
|
||||
G F e a X X b
|
||||
G F e a X X X b
|
||||
G i a X X X b
|
||||
G F i a X X X b
|
||||
& G i a F b G i b F c
|
||||
G i a F b
|
||||
& G i a F b G c
|
||||
& & G ! c G i a F b G i b F c
|
||||
& G i a F b G i c F d
|
||||
& i G a F b i G ! a F ! b
|
||||
& G i a F b G i ! a F ! b
|
||||
U p & q X U r s
|
||||
U p & q X & r F & s X F & u X F & v X F w
|
||||
F & p X & q X F r
|
||||
F & q X U p r
|
||||
G i p U q r
|
||||
F & p X F & q X F & r X F s
|
||||
& & & & G F p G F q G F r G F s G F u
|
||||
| | U p U q r U q U r p U r U p q
|
||||
| | G F a G F b G F c
|
||||
G F a
|
||||
U a U b U c d
|
||||
G U a U b U ! a ! b
|
||||
EOF
|
||||
|
||||
# More examples taken from scheck's test suite.
|
||||
# http://tcs.legacy.ics.tkk.fi/users/tlatvala/scheck/
|
||||
cat >>formulas <<EOF
|
||||
| F X p1 F X p2
|
||||
| | X p7 F p6 & | | t p3 p7 U | f p3 p3
|
||||
F p99
|
||||
X p3
|
||||
X ! p3
|
||||
X t
|
||||
X X X p3
|
||||
F X X X t
|
||||
! G p5
|
||||
| X p0 F p5
|
||||
| F p2 F p9
|
||||
! | G p0 & G p1 F p3
|
||||
& U & X p0 X p4 F p1 X X U X F p5 U p0 X X p3
|
||||
| p3 p5
|
||||
& p1 p6
|
||||
| p1 | p2 p1
|
||||
| & p1 p3 p3
|
||||
p6
|
||||
U p1 ! p2
|
||||
| p5 U p2 p2
|
||||
& p5 U p2 p2
|
||||
U F p5 ! p1
|
||||
U p0 & | p0 p5 p1
|
||||
EOF
|
||||
|
||||
# More examples randomly generated
|
||||
$randltl -l -n 100 a p1 "X" "U" "U12" >> formulas
|
||||
|
||||
# Some examples from scalables formulas
|
||||
$genltl --rv-counter=1..10 --go-theta=1..10 -l >> formulas
|
||||
|
||||
count=`wc -l < formulas`
|
||||
|
||||
test $count -eq 168
|
||||
|
||||
run 0 $ltlfilt --lbt-input formulas > formulas.2
|
||||
run 0 $ltlfilt -l formulas.2 > formulas.3
|
||||
run 0 $ltlfilt -l --lbt-input formulas > formulas.4
|
||||
test `wc -l < formulas.2` -eq 168
|
||||
test `wc -l < formulas.3` -eq 168
|
||||
test `wc -l < formulas.4` -eq 168
|
||||
|
||||
run 0 $ltlfilt formulas.2 --csv-escape --format='%L,%f' > formulas.5
|
||||
run 0 $ltlfilt formulas.5/2 --csv-escape --format='%L,%f' > formulas.6
|
||||
cmp formulas.5 formulas.6
|
||||
|
||||
# Make sure ltl2dstar-style litterals always get quoted.
|
||||
test "`$ltlfilt -l --lbt-input -f 'G F a'`" = 'G F "a"'
|
||||
# Original lbt-style litterals are unquoted.
|
||||
test "`$ltlfilt -l --lbt-input -f 'G F p42'`" = 'G F p42'
|
||||
65
src/tests/length.cc
Normal file
65
src/tests/length.cc
Normal file
|
|
@ -0,0 +1,65 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012 Laboratoire de Recherche et Developement de
|
||||
// l'Epita (LRDE).
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/length.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
void
|
||||
syntax(char *prog)
|
||||
{
|
||||
std::cerr << prog << " formula" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char **argv)
|
||||
{
|
||||
if (argc < 2 || argc > 3)
|
||||
syntax(argv[0]);
|
||||
|
||||
bool boolone = false;
|
||||
if (!strcmp(argv[1], "-b"))
|
||||
{
|
||||
boolone = true;
|
||||
++argv;
|
||||
}
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
|
||||
return 2;
|
||||
|
||||
if (boolone)
|
||||
std::cout << spot::ltl::length_boolone(f1) << std::endl;
|
||||
else
|
||||
std::cout << spot::ltl::length(f1) << std::endl;
|
||||
|
||||
f1->destroy();
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return 0;
|
||||
}
|
||||
39
src/tests/length.test
Executable file
39
src/tests/length.test
Executable file
|
|
@ -0,0 +1,39 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2015 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
len()
|
||||
{
|
||||
test `run 0 ../length "$1"` = $2
|
||||
test `run 0 ../length -b "$1"` = $3
|
||||
}
|
||||
|
||||
len 'a U Xc' 4 4
|
||||
len 'a&b&c' 5 1
|
||||
len 'a|b|c' 5 1
|
||||
len '!a|b|!c' 7 1
|
||||
len '!(!a|b|!c)' 8 1
|
||||
len '!X(!a|b|!c)' 9 3
|
||||
len 'Xa|(b|c)' 6 4
|
||||
len 'Xa&(b|c)' 6 4
|
||||
57
src/tests/lenient.test
Executable file
57
src/tests/lenient.test
Executable file
|
|
@ -0,0 +1,57 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012 Laboratoire de Recherche et Développement de
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
ltlfilt=../../bin/ltlfilt
|
||||
|
||||
cat >input <<EOF
|
||||
(a < b) U (b == c - 1)
|
||||
((a < b) U {b == c - 1})
|
||||
(((a < b) U (b == c - 1)))
|
||||
(((((a < b))) U (b == c - 1)))
|
||||
(((a < b) U (((b == c - 1)))))
|
||||
(((a < b ) U ({( b == c - 1 )})))
|
||||
((((( a < b))) U ( b == c - 1)))
|
||||
((((( a < b))) U { b == c - 1}!))
|
||||
()a
|
||||
EOF
|
||||
|
||||
cat >expected <<EOF
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
"a < b" U "b == c - 1"
|
||||
Xa
|
||||
EOF
|
||||
|
||||
run 0 $ltlfilt --lenient input > output
|
||||
cmp output expected
|
||||
|
||||
|
||||
|
||||
run 2 $ltlfilt --lenient -f 'F( )' 2> stderr
|
||||
grep 'unexpected empty block' stderr
|
||||
36
src/tests/ltlcrossgrind.test
Executable file
36
src/tests/ltlcrossgrind.test
Executable file
|
|
@ -0,0 +1,36 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014 Laboratoire de Recherche et Dévelopement to
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >fake <<EOF
|
||||
#!/bin/sh
|
||||
../../bin/ltl2tgba -s -f "\$1" | sed 's/p0/p1/g'
|
||||
EOF
|
||||
|
||||
chmod +x fake
|
||||
|
||||
run 1 ../../bin/ltlcross -f 'p0 U p1' "./fake %f >%N" \
|
||||
"../../bin/ltl2tgba -s -f %f >%N" --grind=bogus.grind
|
||||
|
||||
echo p0 >exp
|
||||
diff bogus.grind exp
|
||||
246
src/tests/ltlfilt.test
Executable file
246
src/tests/ltlfilt.test
Executable file
|
|
@ -0,0 +1,246 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check several options of ltlfilt
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
checkopt()
|
||||
{
|
||||
cat >exp
|
||||
run 0 ../../bin/ltlfilt "$@" formulas > out
|
||||
diff exp out
|
||||
}
|
||||
|
||||
# The empty lines in the file are meant, we want to make sure that
|
||||
# they are ignored.
|
||||
cat >formulas <<EOF
|
||||
GFa | FGb /* comment to ignore */
|
||||
F(GFa | /* tricky /* comment */)*/ Gb)
|
||||
|
||||
F(b W GFa)
|
||||
GFa | Gb
|
||||
b W GFa
|
||||
!{a;b*;c}!
|
||||
!{a:b[*/*ignore me*/]:c/*ignore this comment*/}
|
||||
a U Fb
|
||||
G(a & Xb)
|
||||
Xa
|
||||
F(a & !Xa & Xb)
|
||||
{a & {b|c} }
|
||||
|
||||
EOF
|
||||
|
||||
checkopt --eventual <<EOF
|
||||
GFa | FGb
|
||||
F(GFa | Gb)
|
||||
F(b W GFa)
|
||||
a U Fb
|
||||
F(a & !Xa & Xb)
|
||||
EOF
|
||||
|
||||
checkopt --universal <<EOF
|
||||
GFa | FGb
|
||||
F(GFa | Gb)
|
||||
GFa | Gb
|
||||
G(a & Xb)
|
||||
EOF
|
||||
|
||||
checkopt --eventual --universal <<EOF
|
||||
GFa | FGb
|
||||
F(GFa | Gb)
|
||||
EOF
|
||||
|
||||
checkopt --stutter-invariant <<EOF
|
||||
GFa | FGb
|
||||
F(GFa | Gb)
|
||||
F(b W GFa)
|
||||
GFa | Gb
|
||||
b W GFa
|
||||
!{a:b[*]:c}
|
||||
a U Fb
|
||||
F(a & !Xa & Xb)
|
||||
a & (b | c)
|
||||
EOF
|
||||
|
||||
checkopt -c --stutter-invariant <<EOF
|
||||
9
|
||||
EOF
|
||||
|
||||
checkopt --simplify <<EOF
|
||||
F(GFa | Gb)
|
||||
F(GFa | Gb)
|
||||
F(b W GFa)
|
||||
GFa | Gb
|
||||
b W GFa
|
||||
!a | X(!b R !c)
|
||||
!{a:b[*]:c}
|
||||
Fb
|
||||
G(a & Xb)
|
||||
Xa
|
||||
F(a & X(!a & b))
|
||||
a & (b | c)
|
||||
EOF
|
||||
|
||||
checkopt --simplify --eventual --unique <<EOF
|
||||
F(GFa | Gb)
|
||||
F(b W GFa)
|
||||
Fb
|
||||
F(a & X(!a & b))
|
||||
EOF
|
||||
|
||||
checkopt --safety <<EOF
|
||||
!({a;b[*];c}!)
|
||||
G(a & Xb)
|
||||
Xa
|
||||
a & (b | c)
|
||||
EOF
|
||||
|
||||
checkopt --obligation <<EOF
|
||||
!({a;b[*];c}!)
|
||||
!{a:b[*]:c}
|
||||
a U Fb
|
||||
G(a & Xb)
|
||||
Xa
|
||||
F(a & !Xa & Xb)
|
||||
a & (b | c)
|
||||
EOF
|
||||
|
||||
checkopt --guarantee <<EOF
|
||||
!{a:b[*]:c}
|
||||
a U Fb
|
||||
Xa
|
||||
F(a & !Xa & Xb)
|
||||
a & (b | c)
|
||||
EOF
|
||||
|
||||
checkopt -v --ltl <<EOF
|
||||
!({a;b[*];c}!)
|
||||
!{a:b[*]:c}
|
||||
EOF
|
||||
|
||||
checkopt -v --stutter-invariant <<EOF
|
||||
!({a;b[*];c}!)
|
||||
G(a & Xb)
|
||||
Xa
|
||||
EOF
|
||||
|
||||
checkopt --equivalent-to 'GFa | FGb' <<EOF
|
||||
GFa | FGb
|
||||
F(GFa | Gb)
|
||||
F(b W GFa)
|
||||
EOF
|
||||
|
||||
|
||||
cat >in <<EOF
|
||||
a & Xb & c
|
||||
a & b & GF(a | c) & FG(a | c)
|
||||
b & GF(a | c) & FG(a | c)
|
||||
G(d & e) | FG(Xf| !c) | h | i
|
||||
b & !Xc & e & (f | g)
|
||||
b & GF(a | c) & !GF!(a | c)
|
||||
EOF
|
||||
|
||||
cat >exp <<EOF
|
||||
p0 & Xp1
|
||||
p0 & p1 & GF(p0 | p2) & FG(p0 | p2)
|
||||
p0 & GFp1 & FGp1
|
||||
p0 | Gp1 | FG(p2 | Xp3)
|
||||
EOF
|
||||
|
||||
run 0 ../../bin/ltlfilt -u --nnf --relabel-bool=pnn in >out
|
||||
diff exp out
|
||||
|
||||
cat >exp <<EOF
|
||||
#define p0 (a && c)
|
||||
#define p1 (b)
|
||||
p0 && Xp1
|
||||
#define p0 (a)
|
||||
#define p1 (b)
|
||||
#define p2 (c)
|
||||
p0 && p1 && []<>(p0 || p2) && <>[](p0 || p2)
|
||||
#define p0 (b)
|
||||
#define p1 (a || c)
|
||||
p0 && []<>p1 && <>[]p1
|
||||
#define p0 (h || i)
|
||||
#define p1 (d && e)
|
||||
#define p2 (!c)
|
||||
#define p3 (f)
|
||||
p0 || []p1 || <>[](p2 || Xp3)
|
||||
EOF
|
||||
|
||||
run 0 ../../bin/ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
|
||||
diff exp out
|
||||
|
||||
cat >exp <<EOF
|
||||
#define p0 ((a=1))
|
||||
#define p1 ((c=1))
|
||||
#define p2 ((b=1))
|
||||
(p0=1) * (p1=1) * (X(p2=1))
|
||||
#define p0 ((a=1))
|
||||
#define p1 ((b=1))
|
||||
#define p2 ((c=1))
|
||||
(p0=1) * (p1=1) * (G(F((p0=1) + (p2=1)))) * (F(G((p0=1) + (p2=1))))
|
||||
#define p0 ((b=1))
|
||||
#define p1 ((a=1))
|
||||
#define p2 ((c=1))
|
||||
(p0=1) * (G(F((p1=1) + (p2=1)))) * (F(G((p1=1) + (p2=1))))
|
||||
#define p0 ((h=1))
|
||||
#define p1 ((i=1))
|
||||
#define p2 ((d=1))
|
||||
#define p3 ((e=1))
|
||||
#define p4 ((c=1))
|
||||
#define p5 ((f=1))
|
||||
(p0=1) + (p1=1) + (G((p2=1) * (p3=1))) + (F(G((p4=0) + (X(p5=1)))))
|
||||
#define p0 ((b=1))
|
||||
#define p1 ((e=1))
|
||||
#define p2 ((f=1))
|
||||
#define p3 ((g=1))
|
||||
#define p4 ((c=1))
|
||||
(p0=1) * (p1=1) * ((p2=1) + (p3=1)) * (X(p4=0))
|
||||
EOF
|
||||
run 0 ../../bin/ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
|
||||
diff exp out
|
||||
|
||||
SPOT_STUTTER_CHECK=0 \
|
||||
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
|
||||
test $? = 2
|
||||
grep 'non-LTL' stderr
|
||||
|
||||
SPOT_STUTTER_CHECK=555 \
|
||||
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
|
||||
test $? = 2
|
||||
grep 'invalid' stderr
|
||||
|
||||
SPOT_STUTTER_CHECK=5 \
|
||||
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}'
|
||||
|
||||
# This one was incorrectly diagnosed as stutter invariant because of a
|
||||
# bug in the bitvectors.
|
||||
../../bin/ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
|
||||
|
||||
|
||||
../../bin/ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
|
||||
grep 'ltlfilt: options --output and --count are incompatible' stderr
|
||||
|
||||
true
|
||||
167
src/tests/ltlgrind.test
Executable file
167
src/tests/ltlgrind.test
Executable file
|
|
@ -0,0 +1,167 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014 Laboratoire de Recherche et Dévelopement to
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
checkopt()
|
||||
{
|
||||
cat >exp
|
||||
run 0 ../../bin/ltlgrind "$@" > out
|
||||
diff exp out
|
||||
}
|
||||
|
||||
checkopt -f 'Xp1 U (p4 | (p3 xor (p4 W p0)))' <<EOF
|
||||
1
|
||||
Xp1
|
||||
p4 | (p3 xor (p4 W p0))
|
||||
Xp1 W (p4 | (p3 xor (p4 W p0)))
|
||||
Xp1 U (p3 xor (p4 W p0))
|
||||
Xp1 U p4
|
||||
Xp1 U (p3 | p4)
|
||||
Xp1 U (p4 | (p4 W p0))
|
||||
Xp1 U (p4 | (p3 & !(p4 W p0)))
|
||||
Xp1 U (p4 | (!p3 & (p4 W p0)))
|
||||
Xp1 U (p4 | (p3 xor p4))
|
||||
Xp1 U (p4 | (p0 xor p3))
|
||||
Xp1 U (!p3 | p4)
|
||||
Xp1 U (p4 | (p3 xor (p4 W 0)))
|
||||
Xp1 U (p4 | !(p4 W p0))
|
||||
p1 U (p4 | (p3 xor (p4 W p0)))
|
||||
1 U (p4 | (p3 xor (p4 W p0)))
|
||||
Xp4 U (p4 | (p3 xor (p4 W p0)))
|
||||
Xp3 U (p4 | (p3 xor (p4 W p0)))
|
||||
Xp0 U (p4 | (p3 xor (p4 W p0)))
|
||||
Xp1 U (p1 | (p3 xor (p1 W p0)))
|
||||
Xp1 U (p3 | (p3 xor (p3 W p0)))
|
||||
Xp1 U (p0 | (p0 xor p3))
|
||||
Xp1 U (p4 | (p1 xor (p4 W p0)))
|
||||
Xp1 U (p4 | (p4 xor (p4 W p0)))
|
||||
Xp1 U (p4 | (p0 xor (p4 W p0)))
|
||||
Xp1 U (p4 | (p3 xor (p4 W p1)))
|
||||
Xp1 U (p4 | (p3 xor (p4 W p3)))
|
||||
EOF
|
||||
|
||||
checkopt -f '(Xp4 R p3) W !p0' --sort <<EOF
|
||||
1
|
||||
!p0
|
||||
Xp4 R p3
|
||||
p3 W !p0
|
||||
Xp4 W !p0
|
||||
(Xp4 R p3) W p0
|
||||
(Xp4 R p3) W 0
|
||||
(p4 R p3) W !p0
|
||||
(0 R p3) W !p0
|
||||
(p3 W Xp4) W !p0
|
||||
(Xp3 R p3) W !p0
|
||||
(Xp0 R p3) W !p0
|
||||
(Xp4 R p4) W !p0
|
||||
(Xp4 R p0) W !p0
|
||||
(Xp4 R p3) W !p4
|
||||
(Xp4 R p3) W !p3
|
||||
EOF
|
||||
|
||||
checkopt -f 'F(!p2 & p3) | Fp0' -n 4 <<EOF
|
||||
F(!p2 & p3)
|
||||
Fp0
|
||||
(!p2 & p3) | Fp0
|
||||
Fp0 | Fp3
|
||||
EOF
|
||||
|
||||
checkopt -f '{(a | b)[*4] & ((a | b)*; c)} <>-> G(d <-> e) xor f' --split-ops \
|
||||
<<EOF
|
||||
{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f & !G(d <-> e))
|
||||
{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (!f & G(d <-> e))
|
||||
{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(d -> e))
|
||||
{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(e -> d))
|
||||
{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(d & e))
|
||||
{{{a | b}}[*4] & {{{a | b}}[*];c}}<>-> (f xor G(!d & !e))
|
||||
{{{{a | b}}[*];c} && {{{a | b}}[*4];[*]}}<>-> (f xor G(d <-> e))
|
||||
{{{a | b}}[*4] && {{{a | b}}[*];c;[*]}}<>-> (f xor G(d <-> e))
|
||||
EOF
|
||||
|
||||
|
||||
checkopt -f '!(!XXp1 M X(p4 U p2))' --rewrite-ops <<EOF
|
||||
!(!XXp1 R X(p4 U p2))
|
||||
!(X(p4 U p2) U !XXp1)
|
||||
!(!XXp1 M X(p4 W p2))
|
||||
EOF
|
||||
|
||||
checkopt -f '!(p0 & !p2 & (p1 W 0))' --remove-multop-operands <<EOF
|
||||
!(!p2 & (p1 W 0))
|
||||
!(p0 & (p1 W 0))
|
||||
!(p0 & !p2)
|
||||
EOF
|
||||
|
||||
checkopt -f '{p1[*..2] | p2[*3..5] | p3[*6..]}[]-> 0' --simplify-bounds <<EOF
|
||||
{p2[*3..5] | p3[*6..] | p1[*0..1]}[]-> 0
|
||||
{p2[*3..5] | p3[*6..] | p1[*]}[]-> 0
|
||||
{p1[*0..2] | p3[*6..] | p2[*2..5]}[]-> 0
|
||||
{p1[*0..2] | p3[*6..] | p2[*0..5]}[]-> 0
|
||||
{p1[*0..2] | p3[*6..] | p2[*3..4]}[]-> 0
|
||||
{p1[*0..2] | p3[*6..] | p2[*3..]}[]-> 0
|
||||
{p1[*0..2] | p2[*3..5] | p3[*5..]}[]-> 0
|
||||
{p1[*0..2] | p2[*3..5] | p3[*]}[]-> 0
|
||||
EOF
|
||||
|
||||
checkopt -f '!F(!X(Xp1 R p2) -> p4)' --remove-one-ap <<EOF
|
||||
!F(!X(Xp2 R p2) -> p4)
|
||||
!F(!X(Xp4 R p2) -> p4)
|
||||
!F(!X(Xp1 R p1) -> p4)
|
||||
!F(!X(Xp1 R p4) -> p4)
|
||||
!F(!X(Xp1 R p2) -> p1)
|
||||
!F(!X(Xp1 R p2) -> p2)
|
||||
EOF
|
||||
|
||||
checkopt -f '!p4 & (p2 | {{!p1}[*]})' --ap-to-const <<EOF
|
||||
0
|
||||
!p4
|
||||
p2 | {{!p1}[*]}
|
||||
!p4 & {{!p1}[*]}
|
||||
p2 & !p4
|
||||
!p4 & (p2 | {[*]})
|
||||
EOF
|
||||
|
||||
|
||||
checkopt -f 'F(XXp0 | (p4 & Gp0))' --remove-ops <<EOF
|
||||
XXp0 | (p4 & Gp0)
|
||||
F(Xp0 | (p4 & Gp0))
|
||||
F((p0 & p4) | XXp0)
|
||||
EOF
|
||||
|
||||
checkopt -f '1 U (p3 <-> p4)' -m 2 <<EOF
|
||||
1
|
||||
0
|
||||
p3
|
||||
p4
|
||||
p3 -> p4
|
||||
p4 -> p3
|
||||
p3 & p4
|
||||
!p4
|
||||
!p3
|
||||
!p3 & !p4
|
||||
1 U p3
|
||||
1 U p4
|
||||
1 U !p3
|
||||
1 U !p4
|
||||
1 U (p3 & !p4)
|
||||
1 U (!p3 & p4)
|
||||
EOF
|
||||
75
src/tests/ltlrel.cc
Normal file
75
src/tests/ltlrel.cc
Normal file
|
|
@ -0,0 +1,75 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developement
|
||||
// de l'Epita (LRDE).
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/relabel.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
|
||||
void
|
||||
syntax(char *prog)
|
||||
{
|
||||
std::cerr << prog << " formula" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char **argv)
|
||||
{
|
||||
if (argc != 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
|
||||
return 2;
|
||||
|
||||
spot::ltl::relabeling_map* m = new spot::ltl::relabeling_map;
|
||||
const spot::ltl::formula* f2 = spot::ltl::relabel_bse(f1, spot::ltl::Pnn, m);
|
||||
f1->destroy();
|
||||
spot::ltl::to_string(f2, std::cout) << '\n';
|
||||
|
||||
|
||||
typedef std::map<std::string, std::string> map_t;
|
||||
map_t sorted_map;
|
||||
for (spot::ltl::relabeling_map::const_iterator i = m->begin();
|
||||
i != m->end(); ++i)
|
||||
sorted_map[spot::ltl::to_string(i->first)] =
|
||||
spot::ltl::to_string(i->second);
|
||||
for (map_t::const_iterator i = sorted_map.begin();
|
||||
i != sorted_map.end(); ++i)
|
||||
std::cout << " " << i->first << " -> "
|
||||
<< i->second << '\n';
|
||||
f2->destroy();
|
||||
delete m;
|
||||
|
||||
spot::ltl::atomic_prop::dump_instances(std::cerr);
|
||||
spot::ltl::unop::dump_instances(std::cerr);
|
||||
spot::ltl::binop::dump_instances(std::cerr);
|
||||
spot::ltl::multop::dump_instances(std::cerr);
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return 0;
|
||||
}
|
||||
79
src/tests/ltlrel.test
Executable file
79
src/tests/ltlrel.test
Executable file
|
|
@ -0,0 +1,79 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013 Laboratoire de Recherche et Dévelopement to
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the constant_term visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
t()
|
||||
{
|
||||
cat > tmp.$$
|
||||
run 0 ../ltlrel "`head -n 1 tmp.$$`" > out.$$
|
||||
sed 1d tmp.$$ > exp.$$
|
||||
diff out.$$ exp.$$
|
||||
}
|
||||
|
||||
t <<EOF
|
||||
a & Xb & c
|
||||
p0 & Xp1
|
||||
p0 -> a & c
|
||||
p1 -> b
|
||||
EOF
|
||||
|
||||
t <<EOF
|
||||
a & b & GF(a | c) & FG(a | c)
|
||||
p0 & p1 & GF(p0 | p2) & FG(p0 | p2)
|
||||
p0 -> a
|
||||
p1 -> b
|
||||
p2 -> c
|
||||
EOF
|
||||
|
||||
t <<EOF
|
||||
b & GF(a | c) & FG(a | c)
|
||||
p0 & GFp1 & FGp1
|
||||
p0 -> b
|
||||
p1 -> a | c
|
||||
EOF
|
||||
|
||||
t <<EOF
|
||||
G(d & e) | FG(Xf| !c) | h | i
|
||||
p0 | Gp1 | FG(p2 | Xp3)
|
||||
p0 -> h | i
|
||||
p1 -> d & e
|
||||
p2 -> !c
|
||||
p3 -> f
|
||||
EOF
|
||||
|
||||
t <<EOF
|
||||
a <-> b
|
||||
p0
|
||||
p0 -> a <-> b
|
||||
EOF
|
||||
|
||||
t <<EOF
|
||||
(a <-> b) & X(b -> c)
|
||||
(p0 <-> p1) & X(p1 -> p2)
|
||||
p0 -> a
|
||||
p1 -> b
|
||||
p2 -> c
|
||||
EOF
|
||||
54
src/tests/lunabbrev.test
Executable file
54
src/tests/lunabbrev.test
Executable file
|
|
@ -0,0 +1,54 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the unabbreviate_logic visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >lunabbrev.txt<<EOF
|
||||
# A few things that do not change
|
||||
a, a
|
||||
1, 1
|
||||
0, 0
|
||||
G a , G a
|
||||
a U b, a U b
|
||||
a & b, a & b
|
||||
a & b, b & a
|
||||
a & b & c, c & a & b
|
||||
a & b & c, b & c & a
|
||||
a & b & a, b & a & b
|
||||
a & b, b & a & b
|
||||
a & b, b & a & a
|
||||
a & b & (c |(f U g)| e), b & a & a & (c | e |(f U g)| e | c) & b
|
||||
# other formulae that do change
|
||||
a ^ b, (a & !b) | (!a & b)
|
||||
a ^ Xb, (!Xb & a) | (!a & Xb) | (Xb & !a)
|
||||
GF a => F G(b), !GFa | F Gb
|
||||
!a <-> Xb, (Xb & !a) | (!!a & !Xb)
|
||||
(a ^ b) | (b ^ c), (c & !b) | (!c & b) | (a & !b) | (!a & b)
|
||||
EOF
|
||||
|
||||
run 0 ../lunabbrev lunabbrev.txt
|
||||
73
src/tests/nenoform.test
Executable file
73
src/tests/nenoform.test
Executable file
|
|
@ -0,0 +1,73 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2014 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the negative_normal_form visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >nenoform.txt<<EOF
|
||||
# A few things that do not change
|
||||
a, a
|
||||
1, 1
|
||||
0, 0
|
||||
!a, !a
|
||||
a U b, a U b
|
||||
a & b, a & b
|
||||
a & b, b & a
|
||||
a & !b & c, c & a & !b
|
||||
a & b & c, b & c & a
|
||||
Xa & b & Xa, b & Xa & b
|
||||
a & b, b & a & b
|
||||
a & !b, !b & a & a
|
||||
a & b & (Xc |(f U !g)| e), b & a & a & (Xc | e |(f U !g)| e | Xc) & b
|
||||
GFa => FGb, FG!a || FGb
|
||||
|
||||
# Basic rewritings
|
||||
!!a, a
|
||||
!!!!!a, !a
|
||||
!Xa, X!a
|
||||
!Fa, G!a
|
||||
!Ga, F!a
|
||||
!(a ^ b), !a&!b | a&b
|
||||
!(a <=> b), (!a&b) | a&!b
|
||||
!(a => b), a&!b
|
||||
!(!a => !b), !a&b
|
||||
!(a U b), !a R !b
|
||||
!(a R b), !a U !b
|
||||
!(!a R !b), a U b
|
||||
!(a & b & c & d & b), !a | !b | !c | !d
|
||||
!(a | b | c | d), !a & !b & !c & !d
|
||||
|
||||
# Nested rewritings
|
||||
!(a U (!b U ((a & b & c) R d))), !a R (b R ((!a | !b | !c) U !d))
|
||||
!(GF a => FG b), GFa & GF!b
|
||||
|
||||
# Rational operators
|
||||
!X{a;b}<>->Fx, X{a;b}[]->G!x
|
||||
!F({a*}<>->{b*}<>->c), G({a*}[]->{b*}[]->!c)
|
||||
EOF
|
||||
|
||||
run 0 ../nenoform nenoform.txt
|
||||
435
src/tests/ngraph.cc
Normal file
435
src/tests/ngraph.cc
Normal file
|
|
@ -0,0 +1,435 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
#include <iostream>
|
||||
#include "graph/ngraph.hh"
|
||||
#include "twa/twa.hh"
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n)
|
||||
{
|
||||
out << " [label=\"" << g.state_data(n) << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned)
|
||||
{
|
||||
out << '\n';
|
||||
}
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n,
|
||||
std::string name)
|
||||
{
|
||||
out << " [label=\"" << name << "\\n" << g.state_data(n) << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned,
|
||||
std::string name)
|
||||
{
|
||||
out << " [label=\"" << name << "\"]\n";
|
||||
}
|
||||
|
||||
|
||||
template <typename SL, typename TL, typename TR>
|
||||
void
|
||||
dot_trans(std::ostream& out, const spot::digraph<SL, TL>&, TR& tr)
|
||||
{
|
||||
out << " [label=\"" << tr.data() << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename SL, typename TR>
|
||||
void
|
||||
dot_trans(std::ostream& out, const spot::digraph<SL, void>&, TR&)
|
||||
{
|
||||
out << '\n';
|
||||
}
|
||||
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot(std::ostream& out, const spot::digraph<SL, TL>& g)
|
||||
{
|
||||
out << "digraph {\n";
|
||||
unsigned c = g.num_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
dot_state(out, g, s);
|
||||
for (auto& t: g.out(s))
|
||||
{
|
||||
out << ' ' << s << " -> " << t.dst;
|
||||
dot_trans(out, g, t);
|
||||
}
|
||||
}
|
||||
out << "}\n";
|
||||
}
|
||||
|
||||
template <typename G1, typename G2, typename G3, typename G4>
|
||||
void
|
||||
dot(std::ostream& out, const spot::named_graph<G1, G2, G3, G4>& g)
|
||||
{
|
||||
out << "digraph {\n";
|
||||
auto& gg = g.graph();
|
||||
unsigned c = gg.num_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
dot_state(out, gg, s, g.get_name(s));
|
||||
for (auto& t: gg.out(s))
|
||||
{
|
||||
out << ' ' << s << " -> " << t.dst;
|
||||
dot_trans(out, gg, t);
|
||||
}
|
||||
}
|
||||
out << "}\n";
|
||||
}
|
||||
|
||||
|
||||
bool g1(const spot::digraph<void, void>& g,
|
||||
unsigned s, int e)
|
||||
{
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s))
|
||||
{
|
||||
(void) t;
|
||||
++f;
|
||||
}
|
||||
return f == e;
|
||||
}
|
||||
|
||||
bool f1()
|
||||
{
|
||||
spot::digraph<void, void> g(3);
|
||||
spot::named_graph<spot::digraph<void, void>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
auto s2 = gg.new_state("s2");
|
||||
auto s3 = gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2");
|
||||
gg.new_transition("s1", "s3");
|
||||
gg.new_transition("s2", "s3");
|
||||
gg.new_transition("s3", "s1");
|
||||
gg.new_transition("s3", "s2");
|
||||
gg.new_transition("s3", "s3");
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
(void) t;
|
||||
++f;
|
||||
}
|
||||
return f == 2
|
||||
&& g1(g, s3, 3)
|
||||
&& g1(g, s2, 1)
|
||||
&& g1(g, s1, 2);
|
||||
}
|
||||
|
||||
|
||||
bool f2()
|
||||
{
|
||||
spot::digraph<int, void> g(3);
|
||||
spot::named_graph<spot::digraph<int, void>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1", 1);
|
||||
gg.new_state("s2", 2);
|
||||
gg.new_state("s3", 3);
|
||||
gg.new_transition("s1", "s2");
|
||||
gg.new_transition("s1", "s3");
|
||||
gg.new_transition("s2", "s3");
|
||||
gg.new_transition("s3", "s2");
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += g.state_data(t.dst);
|
||||
}
|
||||
return f == 5;
|
||||
}
|
||||
|
||||
bool f3()
|
||||
{
|
||||
spot::digraph<void, int> g(3);
|
||||
spot::named_graph<spot::digraph<void, int>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
gg.new_state("s2");
|
||||
gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2", 1);
|
||||
gg.new_transition("s1", "s3", 2);
|
||||
gg.new_transition("s2", "s3", 3);
|
||||
gg.new_transition("s3", "s2", 4);
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.label;
|
||||
}
|
||||
return f == 3 && g.states().size() == 3;
|
||||
}
|
||||
|
||||
bool f4()
|
||||
{
|
||||
spot::digraph<int, int> g(3);
|
||||
spot::named_graph<spot::digraph<int, int>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1", 2);
|
||||
gg.new_state("s2", 3);
|
||||
gg.new_state("s3", 4);
|
||||
gg.new_transition("s1", "s2", 1);
|
||||
gg.new_transition("s1", "s3", 2);
|
||||
gg.new_transition("s2", "s3", 3);
|
||||
gg.new_transition("s3", "s2", 4);
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.label * g.state_data(t.dst);
|
||||
}
|
||||
return f == 11;
|
||||
}
|
||||
|
||||
bool f5()
|
||||
{
|
||||
typedef spot::digraph<void, std::pair<int, float>> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
gg.new_state("s2");
|
||||
gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2", std::make_pair(1, 1.2f));
|
||||
gg.new_transition("s1", "s3", std::make_pair(2, 1.3f));
|
||||
gg.new_transition("s2", "s3", std::make_pair(3, 1.4f));
|
||||
gg.new_transition("s3", "s2", std::make_pair(4, 1.5f));
|
||||
|
||||
int f = 0;
|
||||
float h = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += std::get<0>(t);
|
||||
h += std::get<1>(t);
|
||||
}
|
||||
return f == 3 && (h > 2.49 && h < 2.51);
|
||||
}
|
||||
|
||||
bool f6()
|
||||
{
|
||||
typedef spot::digraph<void, std::pair<int, float>> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
gg.new_state("s2");
|
||||
gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2", 1, 1.2f);
|
||||
gg.new_transition("s1", "s3", 2, 1.3f);
|
||||
gg.new_transition("s2", "s3", 3, 1.4f);
|
||||
gg.new_transition("s3", "s2", 4, 1.5f);
|
||||
|
||||
int f = 0;
|
||||
float h = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.first;
|
||||
h += t.second;
|
||||
}
|
||||
return f == 3 && (h > 2.49 && h < 2.51);
|
||||
}
|
||||
|
||||
bool f7()
|
||||
{
|
||||
typedef spot::digraph<int, int, true> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1", 2);
|
||||
gg.new_state("s2", 3);
|
||||
gg.new_state("s3", 4);
|
||||
gg.new_transition("s1", {"s2", "s3"}, 1);
|
||||
gg.new_transition("s1", {"s3"}, 2);
|
||||
gg.new_transition("s2", {"s3"}, 3);
|
||||
gg.new_transition("s3", {"s2"}, 4);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
for (auto& tt: t.dst)
|
||||
{
|
||||
f += t.label * g.state_data(tt);
|
||||
}
|
||||
}
|
||||
return f == 15;
|
||||
}
|
||||
|
||||
|
||||
struct int_pair
|
||||
{
|
||||
int one;
|
||||
int two;
|
||||
|
||||
friend std::ostream& operator<<(std::ostream& os, int_pair p)
|
||||
{
|
||||
os << '(' << p.one << ',' << p.two << ')';
|
||||
return os;
|
||||
}
|
||||
|
||||
#if __GNUC__ <= 4 && __GNUC_MINOR__ <= 6
|
||||
int_pair(int one, int two)
|
||||
: one(one), two(two)
|
||||
{
|
||||
}
|
||||
|
||||
int_pair()
|
||||
{
|
||||
}
|
||||
#endif
|
||||
};
|
||||
|
||||
bool f8()
|
||||
{
|
||||
typedef spot::digraph<int_pair, int_pair> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
auto s1 = gg.new_state("s1", 2, 4);
|
||||
gg.new_state("s2", 3, 6);
|
||||
gg.new_state("s3", 4, 8);
|
||||
gg.new_transition("s1", "s2", 1, 3);
|
||||
gg.new_transition("s1", "s3", 2, 5);
|
||||
gg.new_transition("s2", "s3", 3, 7);
|
||||
gg.new_transition("s3", "s2", 4, 9);
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.one * g.state_data(t.dst).one;
|
||||
f += t.two * g.state_data(t.dst).two;
|
||||
}
|
||||
return f == 69;
|
||||
}
|
||||
|
||||
struct my_state: public spot::state
|
||||
{
|
||||
public:
|
||||
virtual ~my_state() noexcept
|
||||
{
|
||||
}
|
||||
|
||||
virtual int compare(const spot::state* other) const
|
||||
{
|
||||
auto o = down_cast<const my_state*>(other);
|
||||
assert(o);
|
||||
|
||||
// Do not simply return "other - this", it might not fit in an int.
|
||||
if (o < this)
|
||||
return -1;
|
||||
if (o > this)
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
|
||||
virtual size_t hash() const
|
||||
{
|
||||
return
|
||||
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
|
||||
}
|
||||
|
||||
virtual my_state*
|
||||
clone() const
|
||||
{
|
||||
return const_cast<my_state*>(this);
|
||||
}
|
||||
|
||||
virtual void destroy() const
|
||||
{
|
||||
}
|
||||
|
||||
friend std::ostream& operator<<(std::ostream& os, const my_state&)
|
||||
{
|
||||
return os;
|
||||
}
|
||||
};
|
||||
|
||||
bool f9()
|
||||
{
|
||||
typedef spot::digraph<my_state, int_pair> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
auto s1 = gg.new_state("s1");
|
||||
gg.new_state("s2");
|
||||
auto s3 = gg.new_state("s3");
|
||||
gg.alias_state(s3, "s3b");
|
||||
|
||||
gg.new_transition("s1", "s2", 1, 3);
|
||||
gg.new_transition("s1", "s3", 2, 5);
|
||||
gg.new_transition("s2", "s3b", 3, 7);
|
||||
gg.new_transition("s3", "s2", 4, 9);
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.one + t.two;
|
||||
}
|
||||
|
||||
|
||||
return (f == 11) &&
|
||||
g.state_data(s1).compare(&g.state_data(gg.get_state("s1"))) == 0 &&
|
||||
g.state_data(s1).compare(&g.state_data(gg.get_state("s2"))) != 0;
|
||||
}
|
||||
|
||||
int main()
|
||||
{
|
||||
bool a1 = f1();
|
||||
bool a2 = f2();
|
||||
bool a3 = f3();
|
||||
bool a4 = f4();
|
||||
bool a5 = f5();
|
||||
bool a6 = f6();
|
||||
bool a7 = f7();
|
||||
bool a8 = f8();
|
||||
bool a9 = f9();
|
||||
std::cout << a1 << ' '
|
||||
<< a2 << ' '
|
||||
<< a3 << ' '
|
||||
<< a4 << ' '
|
||||
<< a5 << ' '
|
||||
<< a6 << ' '
|
||||
<< a7 << ' '
|
||||
<< a8 << ' '
|
||||
<< a9 << '\n';
|
||||
return !(a1 && a2 && a3 && a4 && a5 && a6 && a7 && a8 && a9);
|
||||
}
|
||||
96
src/tests/ngraph.test
Executable file
96
src/tests/ngraph.test
Executable file
|
|
@ -0,0 +1,96 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
# While running some benchmark, Tomáš Babiak found that Spot took too
|
||||
# much time (i.e. >1h) to translate those six formulae. It turns out
|
||||
# that the WDBA minimization was performed after the degeneralization
|
||||
# algorithm, while this is not necessary (WDBA will produce a BA, so
|
||||
# we may as well skip degeneralization). Translating these formulae
|
||||
# in the test-suite ensure that they don't take too much time (the
|
||||
# buildfarm will timeout if it does).
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../ngraph > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph {
|
||||
0 [label="s1"]
|
||||
0 -> 1
|
||||
0 -> 2
|
||||
1 [label="s2"]
|
||||
1 -> 2
|
||||
2 [label="s3"]
|
||||
2 -> 0
|
||||
2 -> 1
|
||||
2 -> 2
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1\n1"]
|
||||
0 -> 1
|
||||
0 -> 2
|
||||
1 [label="s2\n2"]
|
||||
1 -> 2
|
||||
2 [label="s3\n3"]
|
||||
2 -> 1
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1"]
|
||||
0 -> 1 [label="1"]
|
||||
0 -> 2 [label="2"]
|
||||
1 [label="s2"]
|
||||
1 -> 2 [label="3"]
|
||||
2 [label="s3"]
|
||||
2 -> 1 [label="4"]
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1\n2"]
|
||||
0 -> 1 [label="1"]
|
||||
0 -> 2 [label="2"]
|
||||
1 [label="s2\n3"]
|
||||
1 -> 2 [label="3"]
|
||||
2 [label="s3\n4"]
|
||||
2 -> 1 [label="4"]
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1\n(2,4)"]
|
||||
0 -> 1 [label="(1,3)"]
|
||||
0 -> 2 [label="(2,5)"]
|
||||
1 [label="s2\n(3,6)"]
|
||||
1 -> 2 [label="(3,7)"]
|
||||
2 [label="s3\n(4,8)"]
|
||||
2 -> 1 [label="(4,9)"]
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1\n"]
|
||||
0 -> 1 [label="(1,3)"]
|
||||
0 -> 2 [label="(2,5)"]
|
||||
1 [label="s2\n"]
|
||||
1 -> 2 [label="(3,7)"]
|
||||
2 [label="s3\n"]
|
||||
2 -> 1 [label="(4,9)"]
|
||||
}
|
||||
1 1 1 1 1 1 1 1 1
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
|
||||
4
src/tests/origin
Normal file
4
src/tests/origin
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
state1, "!b", state2;
|
||||
state2, "a&b", state3;
|
||||
state3, "a", state4 state1;
|
||||
state4, "b", state1;
|
||||
106
src/tests/parse.test
Executable file
106
src/tests/parse.test
Executable file
|
|
@ -0,0 +1,106 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
|
||||
# et Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check that spot::ltl::parse succeed on valid input, and that
|
||||
# dump and dotty will work with the resulting trees. Note that
|
||||
# this doesn't check that the tree is correct w.r.t. the formula.
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
for f in \
|
||||
'0' \
|
||||
'1' \
|
||||
'true' \
|
||||
'false' \
|
||||
'a' \
|
||||
'p11011' \
|
||||
'(p11011)' \
|
||||
'a & b' \
|
||||
'a * _b12' \
|
||||
'a && .b.' \
|
||||
'a + b' \
|
||||
'a3214 | b' \
|
||||
'a /\ b' \
|
||||
'a || b' \
|
||||
'a \/ b' \
|
||||
'a | b' \
|
||||
'_a_ U b' \
|
||||
'a R b' \
|
||||
'a <=> b' \
|
||||
'a <-> b' \
|
||||
'a ^ b' \
|
||||
'a xor b' \
|
||||
'a => b' \
|
||||
'a -> b' \
|
||||
'F b' \
|
||||
'Gb' \
|
||||
'G(b)' \
|
||||
'!G(!b)' \
|
||||
'!b' \
|
||||
'[]b' \
|
||||
'<>b' \
|
||||
'X b' \
|
||||
'()b' \
|
||||
'X"X"' \
|
||||
'X"F"' \
|
||||
'X"G"' \
|
||||
'X"U"' \
|
||||
'X"W"' \
|
||||
'X"R"' \
|
||||
'X"M"' \
|
||||
'long_atomic_proposition_1 U long_atomic_proposition_2' \
|
||||
' ab & ac | ad ^ af' \
|
||||
'((b & a) + a) & d' \
|
||||
'(ab & ac | ad ) <=> af ' \
|
||||
'a U b U c U d U e U f U g U h U i U j U k U l U m' \
|
||||
'(ab & !Xad + ad U ab) & FG p12 /\ GF p13' \
|
||||
'((([]<>()p12)) )' \
|
||||
'a R ome V anille' \
|
||||
'p=0Uq=1' \
|
||||
'((p=1Rq=1)+p=0)UXq=0' \
|
||||
'((p=1Rq=1)*p=0)UXq=0' \
|
||||
'(Gq=1*Fp=0)UXq=0' \
|
||||
'((p=1Mq=1)Wx+p=0)RXq=0' \
|
||||
'((p=1Vq=1)Rx+p=0)WXq=0' \
|
||||
'((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)'
|
||||
|
||||
do
|
||||
if ../ltl2text "$f"; then
|
||||
:
|
||||
else
|
||||
echo "ltl2text failed to parse '$f'"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
if test -n "$DOT"; then
|
||||
run 0 ../ltl2dot "$f" > parse.dot
|
||||
if $DOT -o /dev/null parse.dot; then
|
||||
rm -f parse.dot
|
||||
else
|
||||
rm -f parse.dot
|
||||
echo "dot failed to parse ltl2dot output for '$f'"
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
done
|
||||
50
src/tests/parse_print_test.cc
Normal file
50
src/tests/parse_print_test.cc
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et
|
||||
// Developpement de l'Epita (LRDE)
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
#include "kripkeparse/public.hh"
|
||||
#include "kripke/kripkeprint.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
|
||||
using namespace spot;
|
||||
|
||||
int main(int argc, char** argv)
|
||||
{
|
||||
int return_value = 0;
|
||||
kripke_parse_error_list pel;
|
||||
|
||||
{
|
||||
auto k = kripke_parse(argv[1], pel, make_bdd_dict());
|
||||
if (!pel.empty())
|
||||
{
|
||||
format_kripke_parse_errors(std::cerr, argv[1], pel);
|
||||
return_value = 1;
|
||||
}
|
||||
|
||||
if (!return_value)
|
||||
kripke_save_reachable(std::cout, k);
|
||||
}
|
||||
|
||||
assert(ltl::atomic_prop::instance_count() == 0);
|
||||
assert(ltl::unop::instance_count() == 0);
|
||||
assert(ltl::binop::instance_count() == 0);
|
||||
assert(ltl::multop::instance_count() == 0);
|
||||
return return_value;
|
||||
}
|
||||
112
src/tests/parseerr.test
Executable file
112
src/tests/parseerr.test
Executable file
|
|
@ -0,0 +1,112 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2013, 2014 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check error recovery in parsing. This also checks how the
|
||||
# resulting tree looks like.
|
||||
|
||||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
check()
|
||||
{
|
||||
set +x; run 1 ../ltl2text "$1" >stdout 2>stderr; set -x
|
||||
if test -n "$2"; then
|
||||
echo "$2" >expect
|
||||
else
|
||||
: >expect
|
||||
fi
|
||||
if cmp stdout expect; then
|
||||
:
|
||||
else
|
||||
echo "'$1' parsed as"
|
||||
cat stdout
|
||||
echo "instead of"
|
||||
cat expect
|
||||
exit 1
|
||||
fi
|
||||
|
||||
if test -n "$3"; then
|
||||
echo "$3" >expect
|
||||
if cmp stderr expect; then
|
||||
:
|
||||
else
|
||||
echo "==== Error output was ===="
|
||||
cat stderr
|
||||
echo "==== instead of ===="
|
||||
cat expect
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
}
|
||||
|
||||
# Empty or unparsable strings
|
||||
check '' ''
|
||||
check '+' ''
|
||||
check '/2/3/4/5 a + b /6/7/8/' ''
|
||||
|
||||
|
||||
cat >recover.txt <<EOF
|
||||
# leading and trailing garbage are skipped
|
||||
a U b c, a U b
|
||||
# (check multop merging while we are at it)
|
||||
a & b & c & d e, a & b & c & d
|
||||
a & (b | c) & d should work, a & (b | c) & d
|
||||
# Binop recovery
|
||||
a U, a
|
||||
a U b V c R, a U b V c
|
||||
a &&& b, a & b
|
||||
a &&| b, a | b
|
||||
|
||||
# Recovery inside parentheses
|
||||
a U (b c) U e R (f g <=> h), a U b U e R f
|
||||
a U ((c) U e) R (<=> f g), a U ((c) U e) R (0)
|
||||
|
||||
# Missing parentheses
|
||||
a & (a + b, a & (a + b)
|
||||
a & (a + b c, a & (a + b)
|
||||
a & (+, a & 0
|
||||
a & (, a & 0
|
||||
|
||||
# Invalid ranges
|
||||
{a[*8..1];b}, {a[*1..8];b}
|
||||
{a[=8..1];b}, {a[=1..8];b}
|
||||
{a[->8..1];b}, {a[->1..8];b}
|
||||
{a[->..0];b}, {a[->0..1];b}
|
||||
EOF
|
||||
run 0 ../equals -E recover.txt
|
||||
|
||||
check 'a - b' 'AP(a)' '>>> a - b
|
||||
^
|
||||
syntax error, unexpected $undefined
|
||||
|
||||
>>> a - b
|
||||
^^^
|
||||
ignoring trailing garbage
|
||||
'
|
||||
|
||||
check '{a[*9999999999]}' 'unop(Closure, bunop(Star, AP(a), 0, unbounded))' \
|
||||
'>>> {a[*9999999999]}
|
||||
^^^^^^^^^^
|
||||
value too large ignored
|
||||
'
|
||||
142
src/tests/rand.test
Executable file
142
src/tests/rand.test
Executable file
|
|
@ -0,0 +1,142 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
randltl=../../bin/randltl
|
||||
|
||||
run 0 $randltl -S -n 20 a b c --tree-size=10 \
|
||||
--sere-priorities=and=0,andNLM=0 \
|
||||
--boolean-priorities=equiv=0,implies=0,xor=0,and=0,not=0 \
|
||||
--dump-priorities > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
Use --sere-priorities to set the following SERE priorities:
|
||||
eword 1
|
||||
boolform 1
|
||||
star 1
|
||||
star_b 1
|
||||
fstar 1
|
||||
fstar_b 1
|
||||
and 0
|
||||
andNLM 0
|
||||
or 1
|
||||
concat 1
|
||||
fusion 1
|
||||
Use --boolean-priorities to set the following Boolean formula priorities:
|
||||
ap 3
|
||||
false 1
|
||||
true 1
|
||||
not 0
|
||||
equiv 0
|
||||
implies 0
|
||||
xor 0
|
||||
and 0
|
||||
or 1
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
|
||||
sere='eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0'
|
||||
sere="$sere,or=0,concat=0,fstar=0,fstar_b=0"
|
||||
|
||||
run 0 $randltl -S -n 10000 a b c --tree-size=10..20 \
|
||||
--sere-p=$sere \
|
||||
--boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \
|
||||
--dump-pr > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
Use --sere-priorities to set the following SERE priorities:
|
||||
eword 0
|
||||
boolform 1
|
||||
star 0
|
||||
star_b 0
|
||||
fstar 0
|
||||
fstar_b 0
|
||||
and 0
|
||||
andNLM 0
|
||||
or 0
|
||||
concat 0
|
||||
fusion 0
|
||||
Use --boolean-priorities to set the following Boolean formula priorities:
|
||||
ap 3
|
||||
false 0
|
||||
true 0
|
||||
not 0
|
||||
equiv 0
|
||||
implies 0
|
||||
xor 0
|
||||
and 0
|
||||
or 0
|
||||
EOF
|
||||
diff stdout expected
|
||||
|
||||
|
||||
|
||||
# Disabling all operators will prevent more formulas to be generated.
|
||||
$randltl -S -n 10000 a b c --tree-size=10..20 \
|
||||
--sere-p=$sere \
|
||||
--boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out &&
|
||||
exit 1
|
||||
sort out > out2
|
||||
cat >expected <<EOF
|
||||
a
|
||||
b
|
||||
c
|
||||
EOF
|
||||
|
||||
diff expected out2
|
||||
|
||||
|
||||
# atomic proposition can be implicitly specified using a number
|
||||
$randltl -n 1000 3 --tree-size=10..20 > out
|
||||
grep -q p0 out
|
||||
grep -q p1 out
|
||||
grep -q p2 out
|
||||
grep p3 out && exit 1
|
||||
|
||||
|
||||
# We should be able to generate exactly two formulas with 0 atomic
|
||||
# propositions.
|
||||
run 0 $randltl -n2 0 | sort > out
|
||||
cat >expected <<EOF
|
||||
0
|
||||
1
|
||||
EOF
|
||||
diff out expected
|
||||
|
||||
# requesting more formulas should fail
|
||||
run 2 $randltl -n3 0
|
||||
|
||||
# If more numbers are given, there are interpreted as atomic propositions
|
||||
run 0 $randltl -n1000 0 1 > out
|
||||
grep -q '"0"' out
|
||||
grep -q '"1"' out
|
||||
|
||||
|
||||
run 0 $randltl -n5 2 -o test-all.ltl
|
||||
run 0 $randltl -n5 2 -o test-%L.ltl
|
||||
cat test-1.ltl test-2.ltl test-3.ltl test-4.ltl test-5.ltl > test-cmp.ltl
|
||||
diff test-cmp.ltl test-all.ltl
|
||||
|
||||
|
||||
$randltl 2 --ltl-prio=X 2>stderr && exit 1
|
||||
grep 'failed to parse LTL priorities near X' stderr
|
||||
111
src/tests/readltl.cc
Normal file
111
src/tests/readltl.cc
Normal file
|
|
@ -0,0 +1,111 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/dump.hh"
|
||||
#include "ltlvisit/dotty.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " [-d] formula" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
void
|
||||
dump_instances(const std::string& label)
|
||||
{
|
||||
std::cerr << "=== " << label << " ===" << std::endl;
|
||||
spot::ltl::atomic_prop::dump_instances(std::cerr);
|
||||
spot::ltl::unop::dump_instances(std::cerr);
|
||||
spot::ltl::binop::dump_instances(std::cerr);
|
||||
spot::ltl::multop::dump_instances(std::cerr);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
int exit_code = 0;
|
||||
|
||||
if (argc < 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
bool debug = false;
|
||||
bool debug_ref = false;
|
||||
int formula_index = 1;
|
||||
|
||||
if (!strcmp(argv[1], "-d"))
|
||||
{
|
||||
debug = true;
|
||||
if (argc < 3)
|
||||
syntax(argv[0]);
|
||||
formula_index = 2;
|
||||
}
|
||||
else if (!strcmp(argv[1], "-r"))
|
||||
{
|
||||
debug_ref = true;
|
||||
if (argc < 3)
|
||||
syntax(argv[0]);
|
||||
formula_index = 2;
|
||||
}
|
||||
|
||||
spot::ltl::environment& env(spot::ltl::default_environment::instance());
|
||||
spot::ltl::parse_error_list pel;
|
||||
const spot::ltl::formula* f = spot::ltl::parse(argv[formula_index],
|
||||
pel, env, debug);
|
||||
|
||||
exit_code =
|
||||
spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
|
||||
|
||||
|
||||
if (f)
|
||||
{
|
||||
if (debug_ref)
|
||||
dump_instances("before");
|
||||
|
||||
#ifdef DOTTY
|
||||
spot::ltl::dotty(std::cout, f);
|
||||
#else
|
||||
spot::ltl::dump(std::cout, f);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
f->destroy();
|
||||
|
||||
if (debug_ref)
|
||||
dump_instances("after");
|
||||
}
|
||||
else
|
||||
{
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return exit_code;
|
||||
}
|
||||
328
src/tests/reduc.cc
Normal file
328
src/tests/reduc.cc
Normal file
|
|
@ -0,0 +1,328 @@
|
|||
// -*- coding: utf-8 -*_
|
||||
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
|
||||
// de Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2004, 2006, 2007 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include <string>
|
||||
#include <cstring>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/dump.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
#include "ltlvisit/simplify.hh"
|
||||
#include "ltlvisit/length.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " option formula1 (formula2)?" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
bool readfile = false;
|
||||
bool hidereduc = false;
|
||||
unsigned long sum_before = 0;
|
||||
unsigned long sum_after = 0;
|
||||
spot::ltl::ltl_simplifier_options o(false, false, false, false, false);
|
||||
|
||||
if (argc < 3)
|
||||
syntax(argv[0]);
|
||||
|
||||
if (!strncmp(argv[1], "-f", 3))
|
||||
{
|
||||
readfile = true;
|
||||
++argv;
|
||||
--argc;
|
||||
}
|
||||
|
||||
if (!strncmp(argv[1], "-h", 3))
|
||||
{
|
||||
hidereduc = true;
|
||||
++argv;
|
||||
--argc;
|
||||
}
|
||||
|
||||
switch (atoi(argv[1]))
|
||||
{
|
||||
case 0:
|
||||
o.reduce_basics = true;
|
||||
break;
|
||||
case 1:
|
||||
o.synt_impl = true;
|
||||
break;
|
||||
case 2:
|
||||
o.event_univ = true;
|
||||
break;
|
||||
case 3:
|
||||
o.reduce_basics = true;
|
||||
o.synt_impl = true;
|
||||
o.event_univ = true;
|
||||
break;
|
||||
case 4:
|
||||
o.reduce_basics = true;
|
||||
o.synt_impl = true;
|
||||
break;
|
||||
case 5:
|
||||
o.reduce_basics = true;
|
||||
o.event_univ = true;
|
||||
break;
|
||||
case 6:
|
||||
o.synt_impl = true;
|
||||
o.event_univ = true;
|
||||
break;
|
||||
case 7:
|
||||
o.containment_checks = true;
|
||||
break;
|
||||
case 8:
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
break;
|
||||
case 9:
|
||||
o.reduce_basics = true;
|
||||
o.synt_impl = true;
|
||||
o.event_univ = true;
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
break;
|
||||
case 10:
|
||||
o.reduce_basics = true;
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
break;
|
||||
case 11:
|
||||
o.synt_impl = true;
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
break;
|
||||
case 12:
|
||||
o.reduce_basics = true;
|
||||
o.synt_impl = true;
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
break;
|
||||
case 13:
|
||||
o.event_univ = true;
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
break;
|
||||
case 14:
|
||||
o.reduce_basics = true;
|
||||
o.event_univ = true;
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
break;
|
||||
case 15:
|
||||
o.reduce_basics = true;
|
||||
o.event_univ = true;
|
||||
o.containment_checks = true;
|
||||
o.containment_checks_stronger = true;
|
||||
o.favor_event_univ = true;
|
||||
break;
|
||||
default:
|
||||
return 2;
|
||||
}
|
||||
|
||||
spot::ltl::ltl_simplifier* simp = new spot::ltl::ltl_simplifier(o);
|
||||
o.reduce_size_strictly = true;
|
||||
spot::ltl::ltl_simplifier* simp_size = new spot::ltl::ltl_simplifier(o);
|
||||
|
||||
const spot::ltl::formula* f1 = 0;
|
||||
const spot::ltl::formula* f2 = 0;
|
||||
|
||||
std::ifstream* fin = 0;
|
||||
|
||||
if (readfile)
|
||||
{
|
||||
fin = new std::ifstream(argv[2]);
|
||||
if (!*fin)
|
||||
{
|
||||
std::cerr << "Cannot open " << argv[2] << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
}
|
||||
|
||||
int exit_code = 0;
|
||||
|
||||
next_line:
|
||||
|
||||
if (fin)
|
||||
{
|
||||
std::string input;
|
||||
do
|
||||
{
|
||||
if (!std::getline(*fin, input))
|
||||
goto end;
|
||||
}
|
||||
while (input == "");
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
f1 = spot::ltl::parse(input, p1);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, input, p1))
|
||||
return 2;
|
||||
}
|
||||
else
|
||||
{
|
||||
spot::ltl::parse_error_list p1;
|
||||
f1 = spot::ltl::parse(argv[2], p1);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
|
||||
return 2;
|
||||
}
|
||||
|
||||
if (argc == 4)
|
||||
{
|
||||
if (readfile)
|
||||
{
|
||||
std::cerr << "Cannot read from file and check result." << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
spot::ltl::parse_error_list p2;
|
||||
f2 = spot::ltl::parse(argv[3], p2);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
|
||||
return 2;
|
||||
}
|
||||
|
||||
{
|
||||
const spot::ltl::formula* ftmp1;
|
||||
|
||||
ftmp1 = f1;
|
||||
f1 = simp_size->negative_normal_form(f1, false);
|
||||
ftmp1->destroy();
|
||||
|
||||
int length_f1_before = spot::ltl::length(f1);
|
||||
std::string f1s_before = spot::ltl::to_string(f1);
|
||||
std::string f1l;
|
||||
|
||||
const spot::ltl::formula* input_f = f1;
|
||||
f1 = simp_size->simplify(input_f);
|
||||
if (!simp_size->are_equivalent(input_f, f1))
|
||||
{
|
||||
std::cerr << "Incorrect reduction from `" << f1s_before
|
||||
<< "' to `" << spot::ltl::to_string(f1) << "'."
|
||||
<< std::endl;
|
||||
exit_code = 3;
|
||||
}
|
||||
else
|
||||
{
|
||||
const spot::ltl::formula* maybe_larger = simp->simplify(input_f);
|
||||
f1l = spot::ltl::to_string(maybe_larger);
|
||||
if (!simp->are_equivalent(input_f, maybe_larger))
|
||||
{
|
||||
std::cerr << "Incorrect reduction (reduce_size_strictly=0) from `"
|
||||
<< f1s_before << "' to `" << f1l << "'." << std::endl;
|
||||
exit_code = 3;
|
||||
}
|
||||
maybe_larger->destroy();
|
||||
}
|
||||
|
||||
input_f->destroy();
|
||||
|
||||
int length_f1_after = spot::ltl::length(f1);
|
||||
std::string f1s_after = spot::ltl::to_string(f1);
|
||||
|
||||
std::string f2s = "";
|
||||
if (f2)
|
||||
{
|
||||
ftmp1 = f2;
|
||||
f2 = simp_size->negative_normal_form(f2, false);
|
||||
ftmp1->destroy();
|
||||
f2s = spot::ltl::to_string(f2);
|
||||
}
|
||||
|
||||
sum_before += length_f1_before;
|
||||
sum_after += length_f1_after;
|
||||
|
||||
// If -h is set, we want to print only formulae that have become larger.
|
||||
if (!f2 && (!hidereduc || (length_f1_after > length_f1_before)))
|
||||
{
|
||||
std::cout << length_f1_before << ' ' << length_f1_after
|
||||
<< " '" << f1s_before << "' reduce to '" << f1s_after << '\'';
|
||||
if (f1l != "" && f1l != f1s_after)
|
||||
std::cout << " or (w/o rss) to '" << f1l << '\'';
|
||||
std::cout << '\n';
|
||||
}
|
||||
|
||||
if (f2)
|
||||
{
|
||||
if (f1 != f2)
|
||||
{
|
||||
if (length_f1_after < length_f1_before)
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " KOREDUC " << std::endl;
|
||||
else
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " KOIDEM " << std::endl;
|
||||
exit_code = 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (f1s_before != f1s_after)
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " OKREDUC " << std::endl;
|
||||
else
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " OKIDEM" << std::endl;
|
||||
exit_code = 0;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
if (length_f1_after > length_f1_before)
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
f1->destroy();
|
||||
if (f2)
|
||||
f2->destroy();
|
||||
|
||||
if (fin)
|
||||
goto next_line;
|
||||
}
|
||||
end:
|
||||
|
||||
delete simp_size;
|
||||
delete simp;
|
||||
|
||||
if (fin)
|
||||
{
|
||||
float before = sum_before;
|
||||
float after = sum_after;
|
||||
std::cout << "gain: "
|
||||
<< (1 - (after / before)) * 100 << '%' << std::endl;
|
||||
delete fin;
|
||||
}
|
||||
|
||||
spot::ltl::atomic_prop::dump_instances(std::cerr);
|
||||
spot::ltl::unop::dump_instances(std::cerr);
|
||||
spot::ltl::binop::dump_instances(std::cerr);
|
||||
spot::ltl::multop::dump_instances(std::cerr);
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return exit_code;
|
||||
}
|
||||
47
src/tests/reduc.test
Executable file
47
src/tests/reduc.test
Executable file
|
|
@ -0,0 +1,47 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2012, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2004, 2005, 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the reduc visitor.
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
randltl=../../bin/randltl
|
||||
|
||||
FILE=formulae
|
||||
: > $FILE
|
||||
# for i in 10 11 12 13 14 15 16 17 18 19 20; do
|
||||
for i in 10 12 14 16 18 20; do
|
||||
run 0 $randltl --seed 0 --tree-size $i a b c -n 100 >> $FILE
|
||||
run 0 $randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
|
||||
done
|
||||
|
||||
for opt in 0 1 2 3 7; do
|
||||
run 0 ../reduc -f -h $opt "$FILE"
|
||||
done
|
||||
# Running the above through valgrind is quite slow already.
|
||||
# Don't use valgrind for the next reductions (even slower).
|
||||
for opt in 8 9; do
|
||||
../reduc -f -h $opt "$FILE"
|
||||
done
|
||||
37
src/tests/reduc0.test
Executable file
37
src/tests/reduc0.test
Executable file
|
|
@ -0,0 +1,37 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
# These two reductions used to cause a memory leak.
|
||||
run 0 ../reduc 0 'XFa & FXa' 'XFa'
|
||||
run 0 ../reduc 0 '(Xf W 0) | X(f W 0)' 'XGf'
|
||||
|
||||
# Two incorrect reductions. Those used
|
||||
# to reduce respectively to a W (b && !b) and !a M (b || !b).
|
||||
# But both are wrong. The reduction {a*;r} = a W r seems only
|
||||
# valid if r has a non-empty language.
|
||||
run 0 ../reduc 0 '{a[*];{b && !b}}'
|
||||
run 0 ../reduc 0 '!{a[*];{b && !b}}'
|
||||
|
||||
# Triggered an assert before
|
||||
run 0 ../reduc 0 '(a | (Xa M a))'
|
||||
run 0 ../reduc 0 '(b xor (Xb U b)) <-> e'
|
||||
398
src/tests/reduccmp.test
Executable file
398
src/tests/reduccmp.test
Executable file
|
|
@ -0,0 +1,398 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
|
||||
# Recherche et Developpement de l'Epita (LRDE).
|
||||
# Copyright (C) 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check LTL reductions
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >common.txt <<EOF
|
||||
# No reduction
|
||||
a U b, a U b
|
||||
a R b, a R b
|
||||
a & b, a & b
|
||||
a | b, a | b
|
||||
a & (a U b), a & (a U b)
|
||||
a | (a U b), a | (a U b)
|
||||
|
||||
# Syntactic reduction
|
||||
a & (!b R !a), false
|
||||
(!b R !a) & a, false
|
||||
a & (!b R !a) & c, false
|
||||
c & (!b R !a) & a, false
|
||||
|
||||
a & (!b M !a), false
|
||||
(!b M !a) & a, false
|
||||
a & (!b M !a) & c, false
|
||||
c & (!b M !a) & a, false
|
||||
|
||||
a & (b U a), a
|
||||
(b U a) & a, a
|
||||
a | (b U a), (b U a)
|
||||
(b U a) | a, (b U a)
|
||||
a U (b U a), (b U a)
|
||||
|
||||
a & (b W a), a
|
||||
(b W a) & a, a
|
||||
a | (b W a), (b W a)
|
||||
(b W a) | a, (b W a)
|
||||
a W (b W a), (b W a)
|
||||
|
||||
a & (b U a) & a, a
|
||||
a & (b U a) & a, a
|
||||
a | (b U a) | a, (b U a)
|
||||
a | (b U a) | a, (b U a)
|
||||
a U (b U a), (b U a)
|
||||
|
||||
a & c & (b W a), a & c
|
||||
a & d & c & e & f & g & b & (x W (g & f)), a&b&c&d&e&f&g
|
||||
(F!a & X(!b R a)) | (Ga & X(b U !a)), F!a & X(!b R a)
|
||||
d & ((!a & d) | (a & d)), (!a & d) | (a & d)
|
||||
|
||||
a <-> !a, 0
|
||||
a <-> a, 1
|
||||
a ^ a, 0
|
||||
a ^ !a, 1
|
||||
|
||||
GFa | FGa, GFa
|
||||
XXGa | GFa, GFa
|
||||
GFa & FGa, FGa
|
||||
XXGa & GFa, XXGa
|
||||
|
||||
# Basic reductions
|
||||
X(true), true
|
||||
X(false), false
|
||||
F(true), true
|
||||
F(false), false
|
||||
|
||||
XGF(f), GF(f)
|
||||
|
||||
# not reduced
|
||||
a R (b W G(c)), a R (b W G(c))
|
||||
# not reduced.
|
||||
a M ((a&b) R c), a M ((a&b) R c)
|
||||
# not reduced.
|
||||
(a&b) W (a U c), (a&b) W (a U c)
|
||||
|
||||
# Eventuality and universality class reductions
|
||||
FFa, Fa
|
||||
FGFa, GFa
|
||||
b U Fa, Fa
|
||||
b U GFa, GFa
|
||||
Ga, Ga
|
||||
|
||||
a U XXXFb, XXXFb
|
||||
EOF
|
||||
|
||||
cp common.txt nottau.txt
|
||||
cat >>nottau.txt<<EOF
|
||||
G(true), true
|
||||
G(false), false
|
||||
|
||||
a M 1, Fa
|
||||
a W 0, Ga
|
||||
1 U a, Fa
|
||||
0 R a, Ga
|
||||
|
||||
G(a R b), G(b)
|
||||
|
||||
FX(a), XF(a)
|
||||
GX(a), XG(a)
|
||||
|
||||
(Xf W 0) | X(f W 0), XGf
|
||||
XFa & FXa, XFa
|
||||
|
||||
GF(a | Xb), GF(a | b)
|
||||
GF(a | Fb), GF(a | b)
|
||||
GF(Xa | Fb), GF(a | b)
|
||||
FG(a & Xb), FG(a & b)
|
||||
FG(a & Gb), FG(a & b)
|
||||
FG(Xa & Gb), FG(a & b)
|
||||
|
||||
X(a) U X(b), X(a U b)
|
||||
X(a) R X(b), X(a R b)
|
||||
Xa & Xb, X(a & b)
|
||||
Xa | Xb, X(a | b)
|
||||
|
||||
X(a) M X(b), X(a M b)
|
||||
X(a) W X(b), X(a W b)
|
||||
X(a) M b, b & X(b U a)
|
||||
X(a) R b, b & X(b W a)
|
||||
X(a) U b, b | X(b M a)
|
||||
X(a) W b, b | X(b R a)
|
||||
|
||||
(a U b) & (c U b), (a & c) U b
|
||||
(a R b) & (a R c), a R (b & c)
|
||||
(a U b) | (a U c), a U (b | c)
|
||||
(a R b) | (c R b), (a | c) R b
|
||||
|
||||
Xa & FGb, X(a & FGb)
|
||||
Xa | FGb, X(a | FGb)
|
||||
Xa & GFb, X(a & GFb)
|
||||
Xa | GFb, X(a | GFb)
|
||||
# The following is not reduced to F(a) & GFb. because
|
||||
# (1) is does not help the translate the formula into a
|
||||
# smaller automaton, and ...
|
||||
F(a & GFb), F(a & GFb)
|
||||
# (2) ... it would hinder this useful reduction (that helps to
|
||||
# produce a smaller automaton)
|
||||
F(f1 & GF(f2)) | F(a & GF(b)), F((f1&GFf2)|(a&GFb))
|
||||
# FIXME: Don't we want the opposite rewriting?
|
||||
# rewriting Fa & GFb as F(a & GFb) seems better, but
|
||||
# it not clear how that scales to Fa & Fb & GFc...
|
||||
Fa & GFb, Fa & GFb
|
||||
G(a | GFb), Ga | GFb
|
||||
# The following is not reduced to F(a & c) & GF(b) for the same
|
||||
# reason as above.
|
||||
F(a & GFb & c), F(a & GFb & c)
|
||||
G(a | GFb | c), G(a | c) | GFb
|
||||
|
||||
GFa <=> GFb, G(Fa&Fb)|FG(!a&!b)
|
||||
|
||||
Gb W a, Gb|a
|
||||
Fb M Fa, Fa & Fb
|
||||
|
||||
a U (b | G(a) | c), a W (b | c)
|
||||
a U (G(a)), Ga
|
||||
(a U b) | (a W c), a W (b | c)
|
||||
(a U b) | Ga, a W b
|
||||
|
||||
a R (b & F(a) & c), a M (b & c)
|
||||
a R (F(a)), Fa
|
||||
(a R b) & (a M c), a M (b & c)
|
||||
(a R b) & Fa, a M b
|
||||
|
||||
(a U b) & (c W b), (a & c) U b
|
||||
(a W b) & (c W b), (a & c) W b
|
||||
(a R b) | (c M b), (a | c) R b
|
||||
(a M b) | (c M b), (a | c) M b
|
||||
|
||||
(a R b) | Gb, a R b
|
||||
(a M b) | Gb, a R b
|
||||
(a U b) & Fb, a U b
|
||||
(a W b) & Fb, a U b
|
||||
(a M b) | Gb | (c M b), (a | c) R b
|
||||
|
||||
GFGa, FGa
|
||||
b R Ga, Ga
|
||||
b R FGa, FGa
|
||||
|
||||
G(!a M a) M 1, 0
|
||||
G(!a M a) U 1, 1
|
||||
a R (!a M a), 0
|
||||
a W (!a M a), Ga
|
||||
|
||||
F(a U b), Fb
|
||||
F(a M b), F(a & b)
|
||||
G(a R b), Gb
|
||||
G(a W b), G(a | b)
|
||||
|
||||
Fa W Fb, F(GFa | b)
|
||||
Ga M Gb, FGa & Gb
|
||||
|
||||
a & XGa, Ga
|
||||
a & XG(a&b), (XGb)&(Ga)
|
||||
a & b & XG(a&b), G(a&b)
|
||||
a & b & X(Ga&Gb), G(a&b)
|
||||
a & b & XGa &XG(b), G(a&b)
|
||||
a & b & XGa & XGc, b & Ga & XGc
|
||||
a & b & X(G(a&d) & b) & X(Gc), b & Ga & X(b & G(c&d))
|
||||
a|b|c|X(F(a|b)|F(c)|Gd), F(a|b|c)|XGd
|
||||
b|c|X(F(a|b)|F(c)|Gd), b|c|X(F(a|b|c)|Gd)
|
||||
|
||||
a | (Xa R b) | c, (b W a) | c
|
||||
a | (Xa M b) | c, (b U a) | c
|
||||
a | (Xa M b) | (Xa R c), (b U a) | (c W a)
|
||||
a | (Xa M b) | XF(a), Fa
|
||||
# Gb | Fa ?
|
||||
a | (Xa R b) | XF(a), (b W a) | Fa
|
||||
a & (Xa W b) & c, (b R a) & c
|
||||
a & (Xa U b) & c, (b M a) & c
|
||||
a & (Xa W b) & (Xa U c), (b R a) & (c M a)
|
||||
a & (Xa W b) & XGa, Ga
|
||||
# Fb & Ga ?
|
||||
a & (Xa U b) & XGa, (b M a) & Ga
|
||||
a|(c&b&X((b&c) U a))|d, ((b&c) U a)|d
|
||||
a|(c&X((b&c) W a)&b)|d, ((b&c) W a)|d
|
||||
a&(c|b|X((b|c) M a))&d, ((b|c) M a)&d
|
||||
a&(c|X((b|c) R a)|b)&d, ((b|c) R a)&d
|
||||
g R (f|g|h), (f|h) W g
|
||||
g M (f|g|h), (f|h) U g
|
||||
g U (f&g&h), (f&h) M g
|
||||
g W (f&g&h), (f&h) R g
|
||||
|
||||
# Syntactic implication
|
||||
(a & b) R (a R c), (a & b)R c
|
||||
a R ((a & b) R c), (a & b)R c
|
||||
a R ((a & b) M c), (a & b)M c
|
||||
a M ((a & b) M c), (a & b)M c
|
||||
(a & b) M (a R c), (a & b)M c
|
||||
(a & b) M (a M c), (a & b)M c
|
||||
|
||||
a U ((a & b) U c), a U c
|
||||
(a&c) U (b R (c U d)), b R (c U d)
|
||||
(a&c) U (b R (c W d)), b R (c W d)
|
||||
(a&c) U (b M (c U d)), b M (c U d)
|
||||
(a&c) U (b M (c W d)), b M (c W d)
|
||||
|
||||
(a R c) R (b & a), c R (b & a)
|
||||
(a M c) R (b & a), c R (b & a)
|
||||
|
||||
a W ((a&b) U c), a W c
|
||||
a W ((a&b) W c), a W c
|
||||
|
||||
(a M c) M (b&a), c M (b&a)
|
||||
|
||||
((a&c) U b) U c, b U c
|
||||
((a&c) W b) U c, b U c
|
||||
((a&c) U b) W c, b W c
|
||||
((a&c) W b) W c, b W c
|
||||
(a R b) R (c&a), b R (c&a)
|
||||
(a M b) R (c&a), b R (c&a)
|
||||
(a R b) M (c&a), b M (c&a)
|
||||
(a M b) M (c&a), b M (c&a)
|
||||
|
||||
(a R (b&c)) R (c), (a&b&c) R c
|
||||
(a M (b&c)) R (c), (a&b&c) R c
|
||||
# not reduced
|
||||
(a R (b&c)) M (c), (a R (b&c)) M (c)
|
||||
(a M (b&c)) M (c), (a&b&c) M c
|
||||
(a W (c&b)) W b, (a W (c&b)) | b
|
||||
(a U (c&b)) W b, (a U (c&b)) | b
|
||||
(a U (c&b)) U b, (a U (c&b)) | b
|
||||
# not reduced
|
||||
(a W (c&b)) U b, (a W (c&b)) U b
|
||||
|
||||
# Eventuality and universality class reductions
|
||||
Fa M b, Fa & b
|
||||
GFa M b, GFa & b
|
||||
|
||||
Fa|Xb|GFc, Fa | X(b|GFc)
|
||||
Fa|GFc, F(a|GFc)
|
||||
FGa|GFc, F(Ga|GFc)
|
||||
Ga&Xb&FGc, Ga & X(b&FGc)
|
||||
Ga&Xb&GFc, Ga & X(b&GFc)
|
||||
Ga&GFc, G(a&Fc)
|
||||
G(a|b|GFc|GFd|FGe|FGf), G(a|b)|GF(c|d)|F(Ge|Gf)
|
||||
G(a|b)|GFc|GFd|FGe|FGf, G(a|b)|GF(c|d)|F(Ge|Gf)
|
||||
X(a|b)|GFc|GFd|FGe|FGf, X(a|b|GF(c|d)|F(Ge|Gf))
|
||||
Xa&Xb&GFc&GFd&Ge, X(a&b&G(Fc&Fd))&Ge
|
||||
|
||||
# F comes in front when possible...
|
||||
GFc|GFd|FGe|FGf, F(GF(c|d)|Ge|Gf)
|
||||
G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
|
||||
|
||||
# Because reduccmp will translate the formula,
|
||||
# this also check for an old bug in ltl2tgba_fm.
|
||||
{(c&!c)[->0..1]}!, 0
|
||||
|
||||
# Tricky case that used to break the translator,
|
||||
# because it was translating closer on-the-fly
|
||||
# without pruning the rational automaton.
|
||||
{(c&!c)[=2]}, 0
|
||||
|
||||
{a && b && c*} <>-> d, a&b&c&d
|
||||
{a && b && c[*1..3]} <>-> d, a&b&c&d
|
||||
{a && b && c[->0..2]} <>-> d, a&b&c&d
|
||||
{a && b && c[+]} <>-> d, a&b&c&d
|
||||
{a && b && c[=1]} <>-> d, a&b&c&d
|
||||
{a && b && d[=2]} <>-> d, 0
|
||||
{a && b && d[*2..]} <>-> d, 0
|
||||
{a && b && d[->2..4]} <>-> d, 0
|
||||
{a && { c* : b* : (g|h)*}} <>-> d, a & c & b & (g | h) & d
|
||||
{a && {b;c}} <>-> d, 0
|
||||
{a && {(b;c):e}} <>-> d, 0
|
||||
# until better
|
||||
{a && {b*;c*}} <>-> d, {a && {b*|c*}} <>-> d
|
||||
# until better
|
||||
{a && {(b*;c*):e}} <>-> d, {a && {b*|c*} && e} <>-> d
|
||||
{a && {b*;c}} <>-> d, a & c & d
|
||||
{a && {(b*;c):e}} <>-> d, a & c & d & e
|
||||
{a && {b;c*}} <>-> d, a & b & d
|
||||
{a && {(b;c*):e}} <>-> d, a & b & d & e
|
||||
{{{b1;r1*}&&{b2;r2*}};c}, b1&b2&X{{r1*&&r2*};c}
|
||||
{{b1:r1*}&&{b2:r2*}}, {{b1&&b2}:{r1*&&r2*}}
|
||||
{{r1*;b1}&&{r2*;b2}}, {{r1*&&r2*};{b1&&b2}}
|
||||
{{r1*:b1}&&{r2*:b2}}, {{r1*&&r2*}:{b1&&b2}}
|
||||
{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}, {{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}
|
||||
{{{b1;r1*}&{b2;r2*}};c}, b1&b2&X{{r1*&r2*};c}
|
||||
{{b1:(r1;x1*)}&{b2:(r2;x2*)}}, {{b1&&b2}:{{r1&&r2};{x1*&x2*}}}
|
||||
# Not reduced
|
||||
{{b1:r1*}&{b2:r2*}}, {{b1:r1*}&{b2:r2*}}
|
||||
# Not reduced
|
||||
{{r1*;b1}&{r2*;b2}}, {{r1*;b1}&{r2*;b2}}
|
||||
# Not reduced
|
||||
{{r1*:b1}&{r2*:b2}}, {{r1*:b1}&{r2*:b2}}
|
||||
{{a;b*;c}&{d;e*}&{f*;g}&{h*}}, {{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}
|
||||
{a;(b*;c*;([*0]+{d;e}))*}!, {a;{b|c|{d;e}}*}!
|
||||
{a&b&c*}|->!Xb, (X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))
|
||||
{[*]}[]->b, Gb
|
||||
{a;[*]}[]->b, Gb | !a
|
||||
{[*];a}[]->b, G(b | !a)
|
||||
{a;b;[*]}[]->c, !a | X(!b | Gc)
|
||||
{a;a;[*]}[]->c, !a | X(!a | Gc)
|
||||
{s[*]}[]->b, b W !s
|
||||
{s[+]}[]->b, b W !s
|
||||
{s[*2..]}[]->b, !s | X(b W !s)
|
||||
{a;b*;c;d*}[]->e, !a | X(!b R ((e & X(e W !d)) | !c))
|
||||
{a:b*:c:d*}[]->e, !a | ((!c | (e W !d)) W !b)
|
||||
{a|b*|c|d*}[]->e, (e | !(a | c)) & (e W !b) & (e W !d)
|
||||
{{[*0]|a};b;{[*0]|a};c;e[*]}[]->f,{{[*0]|a};b;{[*0]|a}}[]->X((f&X(f W !e))|!c)
|
||||
|
||||
{a&b&c*}<>->!Xb, (a & b & X!b) | (a & b & c & X(c U !b))
|
||||
{[*]}<>->b, Fb
|
||||
{a;[*]}<>->b, Fb & a
|
||||
{[*];a}<>->b, F(a & b)
|
||||
{a;b;[*]}<>->c, a & X(b & Fc)
|
||||
{a;a;[*]}<>->c, a & X(a & Fc)
|
||||
{s[*]}<>->b, b M s
|
||||
{s[+]}<>->b, b M s
|
||||
{s[*2..]}<>->b, s & X(b M s)
|
||||
{1:a*}!, a
|
||||
{(1;1):a*}!, Xa
|
||||
{a;b*;c;d*}<>->e, a & X(b U (c & (e | X(e M d))))
|
||||
{a:b*:c:d*}<>->e, a & ((c & (e M d)) M b)
|
||||
{a|b*|c|d*}<>->e, ((a | c) & e) | (e M b) | (e M d)
|
||||
{{[*0]|a};b;{[*0]|a};c;e[*]}<>->f, {{[*0]|a};b;{[*0]|a}}<>->X(c&(f|X(f M e)))
|
||||
{a;b[*];c[*];e;f*}, a & X({b*;c*;e})
|
||||
{a;b*;(a* && (b;c));c*}, a & X({b*;(a* && (b;c))})
|
||||
{a;a;b[*2..];b}, a & X(a & X(b & X(b & Xb)))
|
||||
!{a;a;b[*2..];b}, !a | X(!a | X(!b | X(!b | X!b)))
|
||||
!{a;c[*];e;f*}, !a | X!{c[*];e}
|
||||
!{a;b*;(a* && (b;c));c*}, !a | X(!{b*;(a* && (b;c))})
|
||||
{(a;c*;d)|(b;c)}, (a & X{c*;d}) | (b & Xc)
|
||||
!{(a;c*;d)|(b;c)}, (X(!{c*;d}) | !a) & (X!c | !b)
|
||||
(Xc R b) & (Xc W 0), b & XGc
|
||||
{{c*|1}[*0..1]}<>-> v, {{c[+]|1}[*0..1]}<>-> v
|
||||
{{b*;c*}[*3..5]}<>-> v, {{b*;c*}[*0..5]} <>-> v
|
||||
{{b*&c*}[*3..5]}<>-> v, {{b[+]|c[+]}[*0..5]} <>-> v
|
||||
# not reduced
|
||||
{a;(b[*2..4];c*;([*0]+{d;e}))*}!, {a;(b[*2..4];c*;([*0]+{d;e}))*}!
|
||||
{((a*;b)+[*0])[*4..6]}!, {((a*;b))[*0..6]}!
|
||||
{c[*];e[*]}[]-> a, {c[*];e[*]}[]-> a
|
||||
EOF
|
||||
|
||||
run 0 ../reduccmp nottau.txt
|
||||
run 0 ../reductaustr common.txt
|
||||
43
src/tests/reducpsl.test
Executable file
43
src/tests/reducpsl.test
Executable file
|
|
@ -0,0 +1,43 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2011, 2012, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the reduc visitor.
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
randltl=../../bin/randltl
|
||||
|
||||
FILE=formulae
|
||||
: > $FILE
|
||||
for i in 10 12 14 16 18 20; do
|
||||
run 0 $randltl --psl --seed 0 --tree-size $i a b c -n 100 >> $FILE
|
||||
run 0 $randltl --psl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
|
||||
done
|
||||
|
||||
for opt in 0 1 2 3 7; do
|
||||
run 0 ../reduc -f -h $opt "$FILE"
|
||||
done
|
||||
# Running the above through valgrind is quite slow already.
|
||||
# Don't use valgrind for the next reductions (even slower).
|
||||
for opt in 8 9; do
|
||||
../reduc -f -h $opt "$FILE"
|
||||
done
|
||||
48
src/tests/remove_x.test
Executable file
48
src/tests/remove_x.test
Executable file
|
|
@ -0,0 +1,48 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
|
||||
run 0 ../../bin/ltlfilt -q --remove-x -f 'Xa' --equivalent-to 'Ga | (!a & Fa)'
|
||||
|
||||
run 1 ../../bin/ltlfilt -q --stutter-invariant -f 'Xa'
|
||||
|
||||
run 0 ../../bin/ltlfilt -q --stutter-invariant -f 'F(!a & Xa & Xb)'
|
||||
|
||||
run 1 ../../bin/ltlfilt -q --stutter-invariant -f 'F(Xa & Xb)'
|
||||
|
||||
run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xa & Xb)' > out
|
||||
grep -v X out
|
||||
run 0 ../../bin/ltlfilt -q --stutter-invariant -F 'out'
|
||||
|
||||
|
||||
run 1 ../../bin/ltlfilt -q --stutter-invariant -f 'F(!a & Xb)'
|
||||
run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xb)' > out
|
||||
grep -v X out
|
||||
# The output is stutter invariant, even if the input wasn't.
|
||||
run 0 ../../bin/ltlfilt -q --stutter-invariant -F 'out'
|
||||
|
||||
# Ensure remove_x does not depend on clang or gcc recursive calls
|
||||
echo 'F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) |'\
|
||||
' (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b))'\
|
||||
' & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b)))'\
|
||||
' | (!a & b & (G!a | Ga) & (G!b | Gb))))' > expected
|
||||
run 0 ../../bin/ltlfilt --remove-x -f 'F(a & X(!a & b))' > 'out'
|
||||
diff expected out
|
||||
78
src/tests/stutter-ltl.test
Executable file
78
src/tests/stutter-ltl.test
Executable file
|
|
@ -0,0 +1,78 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the stutter-invariant formula detection
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
randltl=../../bin/randltl
|
||||
ltlfilt=../../bin/ltlfilt
|
||||
|
||||
# Use time only if it is available
|
||||
time=time
|
||||
if ($time ls) >/dev/null 2>&1; then
|
||||
:
|
||||
else
|
||||
time=
|
||||
fi
|
||||
|
||||
FILE=formulae
|
||||
rm -f $FILE
|
||||
for i in 10 12 14 16 18 20; do
|
||||
$randltl --seed 0 --tree-size $i a b c -n 100 >> $FILE
|
||||
$randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
|
||||
done
|
||||
|
||||
# We do not check i=0 and i=9, as they are too slow.
|
||||
for i in 1 2 3 4 5 6 7 8; do
|
||||
SPOT_STUTTER_CHECK=$i
|
||||
export SPOT_STUTTER_CHECK
|
||||
$time $ltlfilt --stutter-invariant -F $FILE > res.$i
|
||||
done
|
||||
|
||||
# All results should be equal
|
||||
for i in 2 3 4 5 6 7 8; do
|
||||
diff res.1 res.$i
|
||||
done
|
||||
|
||||
|
||||
# Do a similar test on fewer formulas, so we can cover 0 and 9.
|
||||
cat >$FILE <<EOF
|
||||
F(a & X(!a & b))
|
||||
F(a & X(!a & Xb))
|
||||
F(a & X!a & Xb)
|
||||
F(a & X(a & Xb))
|
||||
F(a & Xb)
|
||||
Xa
|
||||
EOF
|
||||
|
||||
# We do not check i=0 and i=9, as they are too slow.
|
||||
for i in 0 1 2 3 4 5 6 7 8 9; do
|
||||
SPOT_STUTTER_CHECK=$i
|
||||
export SPOT_STUTTER_CHECK
|
||||
$time $ltlfilt --stutter-invariant -F $FILE > res.$i
|
||||
done
|
||||
|
||||
# All results should be equal
|
||||
for i in 1 2 3 4 5 6 7 8 9; do
|
||||
diff res.0 res.$i
|
||||
done
|
||||
119
src/tests/syntimpl.cc
Normal file
119
src/tests/syntimpl.cc
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/lunabbrev.hh"
|
||||
#include "ltlvisit/tunabbrev.hh"
|
||||
#include "ltlvisit/dump.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
#include "ltlvisit/simplify.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlvisit/nenoform.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " formula1 formula2?" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
if (argc < 4)
|
||||
syntax(argv[0]);
|
||||
|
||||
int opt = atoi(argv[1]);
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* ftmp1 = spot::ltl::parse(argv[2], p1);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
|
||||
return 2;
|
||||
|
||||
spot::ltl::parse_error_list p2;
|
||||
const spot::ltl::formula* ftmp2 = spot::ltl::parse(argv[3], p2);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
|
||||
return 2;
|
||||
|
||||
const spot::ltl::formula* f1 = spot::ltl::negative_normal_form(ftmp1);
|
||||
const spot::ltl::formula* f2 = spot::ltl::negative_normal_form(ftmp2);
|
||||
|
||||
std::string f1s = spot::ltl::to_string(f1);
|
||||
std::string f2s = spot::ltl::to_string(f2);
|
||||
|
||||
int exit_return = 0;
|
||||
spot::ltl::ltl_simplifier* c = new spot::ltl::ltl_simplifier;
|
||||
|
||||
switch (opt)
|
||||
{
|
||||
case 0:
|
||||
std::cout << "Test f1 < f2" << std::endl;
|
||||
if (c->syntactic_implication(f1, f2))
|
||||
{
|
||||
std::cout << f1s << " < " << f2s << '\n';
|
||||
exit_return = 1;
|
||||
}
|
||||
break;
|
||||
|
||||
case 1:
|
||||
std::cout << "Test !f1 < f2" << std::endl;
|
||||
if (c->syntactic_implication_neg(f1, f2, false))
|
||||
{
|
||||
std::cout << "!(" << f1s << ") < " << f2s << '\n';
|
||||
exit_return = 1;
|
||||
}
|
||||
break;
|
||||
|
||||
case 2:
|
||||
std::cout << "Test f1 < !f2" << std::endl;
|
||||
if (c->syntactic_implication_neg(f1, f2, true))
|
||||
{
|
||||
std::cout << f1s << " < !(" << f2s << ")\n";
|
||||
exit_return = 1;
|
||||
}
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
||||
spot::ltl::dump(std::cout, f1) << '\n';
|
||||
spot::ltl::dump(std::cout, f2) << '\n';
|
||||
|
||||
f1->destroy();
|
||||
f2->destroy();
|
||||
ftmp1->destroy();
|
||||
ftmp2->destroy();
|
||||
|
||||
delete c;
|
||||
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
|
||||
return exit_return;
|
||||
}
|
||||
99
src/tests/syntimpl.test
Executable file
99
src/tests/syntimpl.test
Executable file
|
|
@ -0,0 +1,99 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check syntactic implication.
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
#
|
||||
#GFa && GFb && FG(!a && !b)
|
||||
run 1 ../syntimpl 0 'a' 'a | b'
|
||||
run 1 ../syntimpl 0 'F(a)' 'F(a | b)'
|
||||
run 1 ../syntimpl 0 'G(a)' 'G(a | b)'
|
||||
run 1 ../syntimpl 0 'GF(a)' 'GF(a | b)'
|
||||
run 1 ../syntimpl 0 'GF(a)' '!FG(!a && !b)'
|
||||
|
||||
run 1 ../syntimpl 0 'Xa' 'X(b U a)'
|
||||
run 1 ../syntimpl 0 'XXa' 'XX(b U a)'
|
||||
|
||||
run 1 ../syntimpl 0 '(e R f)' '(g U f)'
|
||||
run 1 ../syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))'
|
||||
run 1 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
|
||||
|
||||
run 1 ../syntimpl 0 '1' '1'
|
||||
run 1 ../syntimpl 0 '0' '0'
|
||||
|
||||
run 1 ../syntimpl 0 'a' '1'
|
||||
run 1 ../syntimpl 0 'a' 'a'
|
||||
|
||||
run 1 ../syntimpl 0 'a' 'a & 1'
|
||||
|
||||
run 1 ../syntimpl 0 'a & b' 'b'
|
||||
run 1 ../syntimpl 0 'a & b' 'a'
|
||||
|
||||
run 1 ../syntimpl 0 'a' 'a + b'
|
||||
run 1 ../syntimpl 0 'b' 'a + b'
|
||||
|
||||
run 1 ../syntimpl 0 'a + b' '1'
|
||||
|
||||
run 1 ../syntimpl 0 'a' 'b U a'
|
||||
run 1 ../syntimpl 0 'a' 'b U 1'
|
||||
run 1 ../syntimpl 0 'a U b' '1'
|
||||
|
||||
run 1 ../syntimpl 0 'a' '1 R a'
|
||||
run 1 ../syntimpl 0 'a' 'a R 1'
|
||||
run 1 ../syntimpl 0 'a R b' 'b'
|
||||
run 1 ../syntimpl 0 'a R b' '1'
|
||||
|
||||
run 1 ../syntimpl 0 'Xa' 'X(b U a)'
|
||||
run 1 ../syntimpl 0 'X(a R b)' 'Xb'
|
||||
|
||||
run 1 ../syntimpl 0 'a U b' '1 U b'
|
||||
run 1 ../syntimpl 0 'a R b' '1 R b'
|
||||
|
||||
run 1 ../syntimpl 0 'b & (a U b)' 'a U b'
|
||||
run 1 ../syntimpl 0 'a U b' 'c + (a U b)'
|
||||
|
||||
run 0 ../syntimpl 0 'Xa' 'XX(b U a)'
|
||||
run 0 ../syntimpl 0 'XXa' 'X(b U a)'
|
||||
|
||||
run 0 ../syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
|
||||
run 0 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
|
||||
|
||||
run 0 ../syntimpl 0 'a' 'b'
|
||||
run 0 ../syntimpl 0 'a' 'b + c'
|
||||
run 0 ../syntimpl 0 'a + b' 'a'
|
||||
run 0 ../syntimpl 0 'a' 'a & c'
|
||||
run 0 ../syntimpl 0 'a & b' 'c'
|
||||
run 0 ../syntimpl 0 'a' 'a U b'
|
||||
run 0 ../syntimpl 0 'a' 'a R b'
|
||||
run 0 ../syntimpl 0 'a R b' 'a'
|
||||
|
||||
run 0 ../syntimpl 0 'p2' 'p3 || G(p2 && p5)'
|
||||
run 0 ../syntimpl 0 '!(p3 || G(p2 && p5))' '!p2'
|
||||
|
||||
run 0 ../syntimpl 0 'Xc W 0' 'Xc R b'
|
||||
run 1 ../syntimpl 0 '(c&b) W (b&a)' 'a R b'
|
||||
|
||||
exit 0
|
||||
219
src/tests/tgbagraph.test
Executable file
219
src/tests/tgbagraph.test
Executable file
|
|
@ -0,0 +1,219 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
# While running some benchmark, Tomáš Babiak found that Spot took too
|
||||
# much time (i.e. >1h) to translate those six formulae. It turns out
|
||||
# that the WDBA minimization was performed after the degeneralization
|
||||
# algorithm, while this is not necessary (WDBA will produce a BA, so
|
||||
# we may as well skip degeneralization). Translating these formulae
|
||||
# in the test-suite ensure that they don't take too much time (the
|
||||
# buildfarm will timeout if it does).
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../tgbagraph | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label="0"]
|
||||
0 -> 1 [label="p1"]
|
||||
0 -> 2 [label="p2\n{1}"]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label="p1 & p2\n{0}"]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label="p1 | p2\n{0,1}"]
|
||||
2 -> 1 [label="!p1 | p2"]
|
||||
2 -> 2 [label="1\n{0,1}"]
|
||||
}
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label="0"]
|
||||
0 -> 1 [label="p1"]
|
||||
0 -> 2 [label="p2\n{1}"]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label="p1 & p2\n{0}"]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label="p1 | p2\n{0,1}"]
|
||||
}
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label="0"]
|
||||
0 -> 1 [label="p1"]
|
||||
0 -> 2 [label="p2\n{1}"]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label="p1 & p2\n{0}"]
|
||||
2 [label="2"]
|
||||
}
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label="0"]
|
||||
0 -> 1 [label="p1"]
|
||||
0 -> 2 [label="p2\n{1}"]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label="p1 & p2\n{0}"]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label="p1 | p2\n{0,1}"]
|
||||
2 -> 1 [label="!p1 | p2"]
|
||||
2 -> 0 [label="1\n{0,1}"]
|
||||
}
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 1 [label="p1"]
|
||||
0 -> 2 [label="p2\n{1}"]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label="p1 & p2\n{0}"]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label="1\n{0,1}"]
|
||||
2 -> 1 [label="!p1 | p2"]
|
||||
}
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 1 [label="p1"]
|
||||
0 -> 2 [label="p2\n{1}"]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label="p1 & p2\n{0}"]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label="1\n{0,1}"]
|
||||
2 -> 1 [label="!p1 | p2"]
|
||||
3 [label="3"]
|
||||
4 [label="4"]
|
||||
5 [label="5"]
|
||||
6 [label="6"]
|
||||
7 [label="7"]
|
||||
8 [label="8"]
|
||||
9 [label="9"]
|
||||
10 [label="10"]
|
||||
11 [label="11"]
|
||||
12 [label="12"]
|
||||
13 [label="13"]
|
||||
14 [label="14"]
|
||||
15 [label="15"]
|
||||
16 [label="16"]
|
||||
17 [label="17"]
|
||||
18 [label="18"]
|
||||
19 [label="19"]
|
||||
20 [label="20"]
|
||||
21 [label="21"]
|
||||
22 [label="22"]
|
||||
23 [label="23"]
|
||||
24 [label="24"]
|
||||
25 [label="25"]
|
||||
26 [label="26"]
|
||||
27 [label="27"]
|
||||
28 [label="28"]
|
||||
29 [label="29"]
|
||||
30 [label="30"]
|
||||
31 [label="31"]
|
||||
32 [label="32"]
|
||||
33 [label="33"]
|
||||
34 [label="34"]
|
||||
35 [label="35"]
|
||||
36 [label="36"]
|
||||
37 [label="37"]
|
||||
38 [label="38"]
|
||||
39 [label="39"]
|
||||
40 [label="40"]
|
||||
41 [label="41"]
|
||||
42 [label="42"]
|
||||
43 [label="43"]
|
||||
44 [label="44"]
|
||||
45 [label="45"]
|
||||
46 [label="46"]
|
||||
47 [label="47"]
|
||||
48 [label="48"]
|
||||
49 [label="49"]
|
||||
50 [label="50"]
|
||||
51 [label="51"]
|
||||
52 [label="52"]
|
||||
53 [label="53"]
|
||||
54 [label="54"]
|
||||
55 [label="55"]
|
||||
56 [label="56"]
|
||||
57 [label="57"]
|
||||
58 [label="58"]
|
||||
59 [label="59"]
|
||||
60 [label="60"]
|
||||
61 [label="61"]
|
||||
62 [label="62"]
|
||||
63 [label="63"]
|
||||
64 [label="64"]
|
||||
65 [label="65"]
|
||||
66 [label="66"]
|
||||
67 [label="67"]
|
||||
68 [label="68"]
|
||||
69 [label="69"]
|
||||
70 [label="70"]
|
||||
71 [label="71"]
|
||||
72 [label="72"]
|
||||
73 [label="73"]
|
||||
74 [label="74"]
|
||||
75 [label="75"]
|
||||
76 [label="76"]
|
||||
77 [label="77"]
|
||||
78 [label="78"]
|
||||
79 [label="79"]
|
||||
80 [label="80"]
|
||||
81 [label="81"]
|
||||
82 [label="82"]
|
||||
83 [label="83"]
|
||||
84 [label="84"]
|
||||
85 [label="85"]
|
||||
86 [label="86"]
|
||||
87 [label="87"]
|
||||
88 [label="88"]
|
||||
89 [label="89"]
|
||||
90 [label="90"]
|
||||
91 [label="91"]
|
||||
92 [label="92"]
|
||||
93 [label="93"]
|
||||
94 [label="94"]
|
||||
95 [label="95"]
|
||||
96 [label="96"]
|
||||
97 [label="97"]
|
||||
98 [label="98"]
|
||||
99 [label="99"]
|
||||
100 [label="100"]
|
||||
101 [label="101"]
|
||||
102 [label="102"]
|
||||
}
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
80
src/tests/tostring.cc
Normal file
80
src/tests/tostring.cc
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
|
||||
void
|
||||
syntax(char *prog)
|
||||
{
|
||||
std::cerr << prog << " formula1" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char **argv)
|
||||
{
|
||||
if (argc != 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
|
||||
return 2;
|
||||
|
||||
// The string generated from an abstract tree should be parsable
|
||||
// again.
|
||||
|
||||
std::string f1s = spot::ltl::to_string(f1);
|
||||
std::cout << f1s << std::endl;
|
||||
|
||||
const spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, f1s, p1))
|
||||
return 2;
|
||||
|
||||
// This second abstract tree should be equal to the first.
|
||||
|
||||
if (f1 != f2)
|
||||
return 1;
|
||||
|
||||
// It should also map to the same string.
|
||||
|
||||
std::string f2s = spot::ltl::to_string(f2);
|
||||
std::cout << f2s << std::endl;
|
||||
|
||||
if (f2s != f1s)
|
||||
return 1;
|
||||
|
||||
f1->destroy();
|
||||
f2->destroy();
|
||||
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||
assert(spot::ltl::unop::instance_count() == 0);
|
||||
assert(spot::ltl::binop::instance_count() == 0);
|
||||
assert(spot::ltl::multop::instance_count() == 0);
|
||||
return 0;
|
||||
}
|
||||
77
src/tests/tostring.test
Executable file
77
src/tests/tostring.test
Executable file
|
|
@ -0,0 +1,77 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for spot::ltl::tostring.
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../tostring 'a'
|
||||
run 0 ../tostring '1'
|
||||
run 0 ../tostring '0'
|
||||
run 0 ../tostring 'a => b'
|
||||
run 0 ../tostring 'G a '
|
||||
run 0 ../tostring 'a U b'
|
||||
run 0 ../tostring 'a & b'
|
||||
run 0 ../tostring 'a & b & c'
|
||||
run 0 ../tostring 'b & a & b'
|
||||
run 0 ../tostring 'b & a & a'
|
||||
run 0 ../tostring 'a & b & (c |(f U g)| e)'
|
||||
run 0 ../tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ../tostring 'a <=> b'
|
||||
run 0 ../tostring 'a & b & (c |(f U g)| e)'
|
||||
run 0 ../tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
|
||||
run 0 ../tostring 'F"F1"&G"G"&X"X"'
|
||||
run 0 ../tostring 'GFfalse'
|
||||
run 0 ../tostring 'GFtrue'
|
||||
run 0 ../tostring 'p=0Uq=1Ut=1'
|
||||
run 0 ../tostring 'F"FALSE"'
|
||||
run 0 ../tostring 'G"TruE"'
|
||||
run 0 ../tostring 'FFALSE'
|
||||
run 0 ../tostring 'GTruE'
|
||||
run 0 ../tostring 'p=0UFXp=1'
|
||||
run 0 ../tostring 'GF"\GF"'
|
||||
run 0 ../tostring 'GF"foo bar"'
|
||||
run 0 ../tostring 'FFG__GFF'
|
||||
run 0 ../tostring 'X"U"'
|
||||
run 0 ../tostring 'X"W"'
|
||||
run 0 ../tostring 'X"M"'
|
||||
run 0 ../tostring 'X"R"'
|
||||
|
||||
run 0 ../tostring '{a;b;{c && d*};**}|=>G{a*:b*}'
|
||||
run 0 ../tostring 'GF!{{a || c} && b}'
|
||||
run 0 ../tostring 'GF!{{a || c*} && b}<>->{{!a}*}'
|
||||
run 0 ../tostring 'GF{{a || c*} & b[*]}[]->{d}'
|
||||
run 0 ../tostring '{a[*2..3]}'
|
||||
run 0 ../tostring '{a[*0..1]}'
|
||||
run 0 ../tostring '{a[*0..]}'
|
||||
run 0 ../tostring '{a[*..]}'
|
||||
run 0 ../tostring '{a[*1..]}'
|
||||
run 0 ../tostring '{a[+]}'
|
||||
run 0 ../tostring '{[+]}'
|
||||
run 0 ../tostring '{a[*2..3][*4..5]}'
|
||||
|
||||
run 0 ../tostring '{a**}<>->1' > out
|
||||
test "`sed 1q < out `" = '{a[*]}!'
|
||||
60
src/tests/tunabbrev.test
Executable file
60
src/tests/tunabbrev.test
Executable file
|
|
@ -0,0 +1,60 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8-
|
||||
# Copyright (C) 2009, 2010, 2014 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the unabbreviate_ltl visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >tunabbrev.txt<<EOF
|
||||
# A few things that do not change
|
||||
a, a
|
||||
1, 1
|
||||
0, 0
|
||||
a U b, a U b
|
||||
a & b, a & b
|
||||
a & b, b & a
|
||||
a & b & c, c & a & b
|
||||
a & b & c, b & c & a
|
||||
a & b & a, b & a & b
|
||||
a & b, b & a & b
|
||||
a & b, b & a & a
|
||||
a & b & (c |(f U g)| e), b & a & a & (c | e |(f U g)| e | c) & b
|
||||
|
||||
# same as in lunabbrev.test:
|
||||
a ^ b, (a & !b) | (!a & b)
|
||||
a ^ Xb, (!Xb & a) | (!a & Xb) | (Xb & !a)
|
||||
!a <-> Xb, (Xb & !a) | (!!a & !Xb)
|
||||
(a ^ b) | (b ^ c), (c & !b) | (!c & b) | (a & !b) | (!a & b)
|
||||
|
||||
# LTL unabbreviations:
|
||||
G a , false R a
|
||||
GF a => F G(b), !(false R (true U a)) | (true U (false V b))
|
||||
GGGGa, false V a
|
||||
FFFfalse, 0
|
||||
FFFf, true U f
|
||||
EOF
|
||||
|
||||
run 0 ../tunabbrev tunabbrev.txt
|
||||
41
src/tests/tunenoform.test
Executable file
41
src/tests/tunenoform.test
Executable file
|
|
@ -0,0 +1,41 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2003 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for unabbreviate_ltl + negative_normal_form visitors
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
cat >tunenoform.txt<<EOF
|
||||
!(a ^ b), (a|!b) & (!a|b)
|
||||
!(a <=> b), (a|b) & (!a|!b)
|
||||
!(a => b), a&!b
|
||||
!(!a => !b), !a&b
|
||||
!Fa, false R !a
|
||||
!G!a, true U a
|
||||
!(GF a => FG b), (0 R (1 U a)) & (0 R (1 U !b))
|
||||
EOF
|
||||
|
||||
run 0 ../tunenoform tunenoform.txt
|
||||
95
src/tests/twagraph.cc
Normal file
95
src/tests/twagraph.cc
Normal file
|
|
@ -0,0 +1,95 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
//
|
||||
// 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
#include <iostream>
|
||||
#include "twa/twagraph.hh"
|
||||
#include "twaalgos/dotty.hh"
|
||||
#include "ltlenv/defaultenv.hh"
|
||||
|
||||
void f1()
|
||||
{
|
||||
auto d = spot::make_bdd_dict();
|
||||
|
||||
auto& e = spot::ltl::default_environment::instance();
|
||||
|
||||
auto tg = make_twa_graph(d);
|
||||
|
||||
auto* f1 = e.require("p1");
|
||||
auto* f2 = e.require("p2");
|
||||
bdd p1 = bdd_ithvar(d->register_proposition(f1, tg));
|
||||
bdd p2 = bdd_ithvar(d->register_proposition(f2, tg));
|
||||
tg->acc().add_sets(2);
|
||||
f1->destroy();
|
||||
f2->destroy();
|
||||
|
||||
auto s1 = tg->new_state();
|
||||
auto s2 = tg->new_state();
|
||||
auto s3 = tg->new_state();
|
||||
tg->new_transition(s1, s1, bddfalse, 0U);
|
||||
tg->new_transition(s1, s2, p1, 0U);
|
||||
tg->new_transition(s1, s3, p2, tg->acc().mark(1));
|
||||
tg->new_transition(s2, s3, p1 & p2, tg->acc().mark(0));
|
||||
tg->new_transition(s3, s1, p1 | p2, tg->acc().marks({0, 1}));
|
||||
tg->new_transition(s3, s2, p1 >> p2, 0U);
|
||||
tg->new_transition(s3, s3, bddtrue, tg->acc().marks({0, 1}));
|
||||
|
||||
spot::dotty_reachable(std::cout, tg);
|
||||
|
||||
{
|
||||
auto i = tg->get_graph().out_iteraser(s3);
|
||||
++i;
|
||||
i.erase();
|
||||
i.erase();
|
||||
assert(!i);
|
||||
spot::dotty_reachable(std::cout, tg);
|
||||
}
|
||||
|
||||
{
|
||||
auto i = tg->get_graph().out_iteraser(s3);
|
||||
i.erase();
|
||||
assert(!i);
|
||||
spot::dotty_reachable(std::cout, tg);
|
||||
}
|
||||
|
||||
auto all = tg->acc().marks({0, 1});
|
||||
tg->new_transition(s3, s1, p1 | p2, all);
|
||||
tg->new_transition(s3, s2, p1 >> p2, 0U);
|
||||
tg->new_transition(s3, s1, bddtrue, all);
|
||||
|
||||
std::cerr << tg->num_transitions() << '\n';
|
||||
assert(tg->num_transitions() == 7);
|
||||
|
||||
spot::dotty_reachable(std::cout, tg);
|
||||
tg->merge_transitions();
|
||||
spot::dotty_reachable(std::cout, tg);
|
||||
|
||||
std::cerr << tg->num_transitions() << '\n';
|
||||
assert(tg->num_transitions() == 5);
|
||||
|
||||
// Add enough states so that the state vector is reallocated.
|
||||
for (unsigned i = 0; i < 100; ++i)
|
||||
tg->new_state();
|
||||
spot::dotty_reachable(std::cout, tg);
|
||||
}
|
||||
|
||||
int main()
|
||||
{
|
||||
f1();
|
||||
}
|
||||
36
src/tests/unabbrevwm.test
Executable file
36
src/tests/unabbrevwm.test
Executable file
|
|
@ -0,0 +1,36 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2015 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check for the unabbreviate_logic visitor
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
# Removing W,M in this formula caused a segfault at some point.
|
||||
run 0 ../../bin/ltlfilt --remove-wm >out <<EOF
|
||||
(!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
|
||||
(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
|
||||
EOF
|
||||
|
||||
# The first formula will be simplified to the second, so after uniq
|
||||
# the output should have one line.
|
||||
test `uniq out | wc -l` = 1
|
||||
76
src/tests/utf8.test
Executable file
76
src/tests/utf8.test
Executable file
|
|
@ -0,0 +1,76 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Make sure
|
||||
|
||||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
# ----
|
||||
run 0 ../ltl2text '□◯a' >out
|
||||
echo 'unop(G, unop(X, AP(a)))' > exp
|
||||
cmp out exp
|
||||
|
||||
# ----
|
||||
run 0 ../ltl2text '□◯"αβγ"' >out
|
||||
echo 'unop(G, unop(X, AP(αβγ)))' > exp
|
||||
cmp out exp
|
||||
|
||||
|
||||
# ----
|
||||
set +x
|
||||
run 1 ../ltl2text '□)◯a' 2>err
|
||||
set -x
|
||||
cat >exp <<EOF
|
||||
>>> □)◯a
|
||||
^
|
||||
syntax error, unexpected closing parenthesis
|
||||
|
||||
>>> □)◯a
|
||||
^
|
||||
missing right operand for "always operator"
|
||||
|
||||
>>> □)◯a
|
||||
^^^
|
||||
ignoring trailing garbage
|
||||
|
||||
EOF
|
||||
cmp exp err
|
||||
|
||||
# ----
|
||||
set +x
|
||||
run 1 ../ltl2text '"αβγ"X' 2>err
|
||||
set -x
|
||||
cat >exp <<EOF
|
||||
>>> "αβγ"X
|
||||
^
|
||||
syntax error, unexpected next operator
|
||||
|
||||
>>> "αβγ"X
|
||||
^
|
||||
ignoring trailing garbage
|
||||
|
||||
EOF
|
||||
cmp exp err
|
||||
|
||||
|
||||
../../bin/randltl --psl -8 --seed 0 --tree-size 16 a b c -n 100 > formulae
|
||||
../reduc -f -h 0 formulae
|
||||
61
src/tests/uwrm.test
Executable file
61
src/tests/uwrm.test
Executable file
|
|
@ -0,0 +1,61 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
# Check LTL reductions for U, W, M and R.
|
||||
# These formulas comes from an appendix of tl/tl.tex
|
||||
|
||||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
cat >input.txt<<EOF
|
||||
# Equivalences with U
|
||||
1 U f, Ff
|
||||
!F!f, !(1 U!f), Gf
|
||||
(f U g)|(G f), (f U g) | !(1 U ! f), f U (g | G f), f U (g | !(1 U !f)), f W g
|
||||
g U (f & g), f M g
|
||||
g W (f & g), (g U (f & g)) | !(1 U ! g), g U ((f & g) | !(1 U ! g)), f R g
|
||||
|
||||
# Equivalences with W
|
||||
!G!f, !((! f) W 0), Ff
|
||||
0 R f, f W 0, Gf
|
||||
(f W g) & (F g), (f W g) & !((! g) W 0), f U g
|
||||
(g W (f & g)) & (F f), (g W (f & g)) & !((!f) W 0), f M g
|
||||
g W (f & g), f R g
|
||||
|
||||
# Equivalences with R
|
||||
!G!f, !(0 R !f), Ff
|
||||
0 R f, Gf
|
||||
# (((X g) R f) & F g) | g, (((X g) R f ) & (!(0 R ! g))) | g, f U g
|
||||
((X g) R f) | g, g R (f | g), f W g
|
||||
(f R g) & F f, (f R g) & !(0 R !f), f R (g & F f), f R (g & !(0 R !f)), f M g
|
||||
|
||||
# Equivalences with M
|
||||
f M 1, Ff
|
||||
!F!f, !((!f) M 1), Gf
|
||||
((X g) M f) | g, g M (f | g), f U g
|
||||
(f U g) | G f, ((X g) M f) | g | !((! f ) M 1), f W g
|
||||
(f M g) | G g, (f M g) | !((! g) M 1), f R g
|
||||
|
||||
# Example from tl.tex
|
||||
#(((f U (Xg & f))|!(1 U !f))&(1 U Xg)) | g, f U g
|
||||
EOF
|
||||
|
||||
run 0 ../reduccmp input.txt
|
||||
Loading…
Add table
Add a link
Reference in a new issue