alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbatest/tripprod.test, src/tgbatest/explprod.test:

Browse source 
Sort out some possible inversions in the output.
This commit is contained in:
Alexandre Duret-Lutz 2003-06-22 20:08:30 +00:00
parent 725dacb4e8
commit fbbfda43f2
3 changed files with 26 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

15
ChangeLog
View file

@ -1,14 +1,19 @@
2003-06-22 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbatest/tripprod.test, src/tgbatest/explprod.test:
Sort out some possible inversions in the output.
2003-06-19 Alexandre Duret-Lutz <aduret@src.lip6.fr> 2003-06-19 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddconcretefactory.cc * src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the (tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the
formulae used as keys in prom_. formulae used as keys in prom_.
(tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::create_promise): Delete.
(tgba_bdd_concrete_factory::declare_promise, (tgba_bdd_concrete_factory::declare_promise,
tgba_bdd_concrete_factory::finish): New functions. tgba_bdd_concrete_factory::finish): New functions.
* src/tgba/tgbabddconcretefactory.hh * src/tgba/tgbabddconcretefactory.hh
(tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::create_promise): Delete.
(tgba_bdd_concrete_factory::declare_promise, (tgba_bdd_concrete_factory::declare_promise,
tgba_bdd_concrete_factory::finish): New functions. tgba_bdd_concrete_factory::finish): New functions.
(tgba_bdd_concrete_factory::prom_): New map. (tgba_bdd_concrete_factory::prom_): New map.
* src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust

9
src/tgbatest/explprod.test
View file

@ -18,12 +18,17 @@ EOF
cat >expected <<EOF cat >expected <<EOF
"s1 * s1", "s3 * s2", a b, "p2"; "s1 * s1", "s3 * s2", a b, "p2";
"s1 * s1", "s2 * s2", b, "p2" "p1"; "s1 * s1", "s2 * s2", b, "p1" "p2";
"s2 * s2", "s3 * s1", c a, "p3"; "s2 * s2", "s3 * s1", a c, "p3";
EOF EOF
./explprod input1 input2 > stdout ./explprod input1 input2 > stdout
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/c a/a c/g;s/b a/a b/g;s/"p2" "p1"/"p1" "p2"/g' stdout > tmp_ &&
mv tmp_ stdout
cat stdout cat stdout
diff stdout expected diff stdout expected
rm input1 input2 stdout expected rm input1 input2 stdout expected

13
src/tgbatest/tripprod.test
View file

@ -25,15 +25,20 @@ EOF
cat >expected <<EOF cat >expected <<EOF
"s1 * s1 * s1", "s3 * s2 * s2", a b, "p2"; "s1 * s1 * s1", "s3 * s2 * s2", a b, "p2";
"s1 * s1 * s1", "s2 * s2 * s2", a b, "p2" "p1"; "s1 * s1 * s1", "s2 * s2 * s2", a b, "p1" "p2";
"s2 * s2 * s2", "s3 * s1 * s3", c a, "p3" "p4"; "s2 * s2 * s2", "s3 * s1 * s3", a c, "p3" "p4";
"s1 * s1 * s1", "s3 * s2 * s3", a b, "p2"; "s1 * s1 * s1", "s3 * s2 * s3", a b, "p2";
"s1 * s1 * s1", "s2 * s2 * s3", b, "p2" "p1"; "s1 * s1 * s1", "s2 * s2 * s3", b, "p1" "p2";
"s2 * s2 * s3", "s3 * s1 * s2", c a, "p3" "p4"; "s2 * s2 * s3", "s3 * s1 * s2", a c, "p3" "p4";
EOF EOF
./tripprod input1 input2 input3 > stdout ./tripprod input1 input2 input3 > stdout
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/c a/a c/g;s/b a/a b/g;s/"p2" "p1"/"p1" "p2"/g;s/"p4" "p3"/"p3" "p4"/g' stdout > tmp_ &&
mv tmp_ stdout
cat stdout cat stdout
diff stdout expected diff stdout expected
rm input1 input2 input3 stdout expected rm input1 input2 input3 stdout expected