From 68adcc70fa958659c88d01b21e48bb824ff695eb Mon Sep 17 00:00:00 2001 From: Thibaud Michaud Date: Tue, 9 Dec 2014 05:01:40 +0100 Subject: [PATCH] Use autfilt --isomorph instead of a diff in some tests * src/tgbatest/degenlskip.test, src/tgbatest/explpro2.test src/tgbatest/explpro3.test, src/tgbatest/explpro4.test src/tgbatest/explprod.test, src/tgbatest/neverclaimread.test src/tgbatest/tripprod.test, src/tgbatest/readsave.test: Here. --- src/tgbatest/degenlskip.test | 77 +++++++++++++++++------------- src/tgbatest/explpro2.test | 3 +- src/tgbatest/explpro3.test | 3 +- src/tgbatest/explpro4.test | 3 +- src/tgbatest/explprod.test | 3 +- src/tgbatest/neverclaimread.test | 80 ++++++++++++++++---------------- src/tgbatest/readsave.test | 6 +-- src/tgbatest/tripprod.test | 3 +- 8 files changed, 91 insertions(+), 87 deletions(-) diff --git a/src/tgbatest/degenlskip.test b/src/tgbatest/degenlskip.test index b15c18cd4..c2c81de3c 100755 --- a/src/tgbatest/degenlskip.test +++ b/src/tgbatest/degenlskip.test @@ -25,47 +25,58 @@ set -e # Make sure degen-skip=0 and degen-skip=1 produce the expected # automata for 'GFa & GFb' -../../bin/ltl2tgba -B 'GFa & GFb' > out1 -../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' > out2 -../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' > out3 +../../bin/ltl2tgba -B 'GFa & GFb' --hoa > out1 +../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' --hoa > out2 +../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' --hoa > out3 diff out1 out2 cmp out2 out3 && exit 1 cat <expected2 -digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0", peripheries=2] - 1 -> 1 [label="a & b\n{0}"] - 1 -> 2 [label="!b\n{0}"] - 1 -> 3 [label="!a & b\n{0}"] - 2 [label="1"] - 2 -> 1 [label="a & b"] - 2 -> 2 [label="!b"] - 2 -> 3 [label="!a & b"] - 3 [label="2"] - 3 -> 1 [label="a"] - 3 -> 3 [label="!a"] -} +HOA: v1 +name: "G(Fa & Fb)" +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete deterministic +--BODY-- +State: 0 {0} +[0&1] 0 +[!1] 1 +[!0&1] 2 +State: 1 +[0&1] 0 +[!1] 1 +[!0&1] 2 +State: 2 +[0] 0 +[!0] 2 +--END-- EOF cat <expected3 -digraph G { - 0 [label="", style=invis, height=0] - 0 -> 1 - 1 [label="0", peripheries=2] - 1 -> 2 [label="1\n{0}"] - 2 [label="1"] - 2 -> 2 [label="!b"] - 2 -> 3 [label="b"] - 3 [label="2"] - 3 -> 1 [label="a"] - 3 -> 3 [label="!a"] -} +HOA: v1 +name: "G(Fa & Fb)" +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete deterministic +--BODY-- +State: 0 {0} +[t] 1 +State: 1 +[!1] 1 +[1] 2 +State: 2 +[0] 0 +[!0] 2 +--END-- EOF -# FIXME: use are-isomorphic once it is available -diff out2 expected2 -diff out3 expected3 +test -n "`../../bin/autfilt -F out2 --isomorph expected2`" +test -n "`../../bin/autfilt -F out3 --isomorph expected3`" diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test index 8691e99cd..599c39b7f 100755 --- a/src/tgbatest/explpro2.test +++ b/src/tgbatest/explpro2.test @@ -78,7 +78,6 @@ State: 2 EOF run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout -# FIXME: Use are-isomorphic -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" rm input1 input2 stdout expected diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test index 045069d52..4009ac185 100755 --- a/src/tgbatest/explpro3.test +++ b/src/tgbatest/explpro3.test @@ -78,6 +78,5 @@ State: 2 EOF run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout -# FIXME: Use are-isomorphic -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" rm input1 input2 stdout expected diff --git a/src/tgbatest/explpro4.test b/src/tgbatest/explpro4.test index 150fabb1e..0ef9f84b7 100755 --- a/src/tgbatest/explpro4.test +++ b/src/tgbatest/explpro4.test @@ -72,7 +72,6 @@ State: 0 EOF run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout -# FIXME: Use are-isomorphic -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" rm input1 input2 stdout expected diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index 9385ec6e5..bc856712c 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -97,7 +97,6 @@ State: 0 EOF run 0 ../../bin/autfilt input1 --product input2 --hoa --small | tee stdout -# FIXME: Use are-isomorphic -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" rm input1 input2 stdout expected diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 189855a4c..2645b1daf 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -44,30 +44,30 @@ skip } EOF -run 0 ../ltl2tgba -XN input > stdout +run 0 ../ltl2tgba -XN -H input > stdout cat >expected < 1 - 1 [label="0"] - 1 -> 1 [label="1"] - 1 -> 2 [label="p0 & p1"] - 2 [label="1"] - 2 -> 1 [label="!p1"] - 2 -> 2 [label="!p1"] - 2 -> 3 [label="p1 & !p0"] - 3 [label="2", peripheries=2] - 3 -> 3 [label="1\n{0}"] -} +HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[t] 0 +[0&1] 1 +State: 1 +[!1] 0 +[!1] 1 +[!0&1] 2 +State: 2 {0} +[t] 2 +--END-- EOF -# Sort out some possible inversions in the output. -# (The order is not guaranteed by SPOT.) -sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \ - > tmp_ && mv tmp_ stdout -# FIXME: use are-isomorphic once it is available -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" rm input stdout expected @@ -89,30 +89,30 @@ od; } EOF -run 0 ../ltl2tgba -XN input > stdout +run 0 ../ltl2tgba -XN -H input > stdout cat >expected < 1 - 1 [label="0"] - 1 -> 1 [label="1"] - 1 -> 2 [label="p0 & p1"] - 2 [label="1"] - 2 -> 1 [label="!p1"] - 2 -> 2 [label="!p1"] - 2 -> 3 [label="p1 & !p0"] - 3 [label="2", peripheries=2] - 3 -> 3 [label="1\n{0}"] -} +HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[t] 0 +[0&1] 1 +State: 1 +[!1] 0 +[!1] 1 +[!0&1] 2 +State: 2 {0} +[t] 2 +--END-- EOF -# Sort out some possible inversions in the output. -# (The order is not guaranteed by SPOT.) -sed -e 's/!p0 & p1/p1 \& !p0/g' -e 's/p1 & p0/p0 \& p1/g' stdout \ - > tmp_ && mv tmp_ stdout -# FIXME: use are-isomorphic once it is available -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" rm input stdout expected diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 5fa3ce51e..88b515057 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -89,17 +89,15 @@ State: 1 EOF run 0 ../../bin/autfilt --merge-transitions --hoa input > stdout -# FIXME: use are-isomorphic once it is available cat stdout -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" # Likewise, with a randomly generated TGBA. run 0 ../../bin/randaut -S 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee input # the first read-write can renumber the states run 0 $autfilt --hoa --merge-transitions input > stdout -# FIXME: use are-ismorphic -# diff input stdout +test -n "`../../bin/autfilt -F input --isomorph stdout`" # But this second output should be the same as the first run 0 $autfilt --hoa stdout > stdout2 diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test index a37abdfd3..396c7aad3 100755 --- a/src/tgbatest/tripprod.test +++ b/src/tgbatest/tripprod.test @@ -107,7 +107,6 @@ EOF run 0 ../../bin/autfilt input1 --product input2 --product input3 --hoa | tee stdout -# FIXME: Use are-isomorphic -diff stdout expected +test -n "`../../bin/autfilt -F stdout --isomorph expected`" rm input1 input2 input3 stdout expected