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

@@ -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 'GFa & GFb' --hoa > out1
-../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' > out2
+../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' --hoa > out2
-../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' > out3
+../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' --hoa > out3
 
 diff out1 out2
 cmp out2 out3 && exit 1
 
 cat <<EOF >expected2
-digraph G {
+HOA: v1
-  0 [label="", style=invis, height=0]
+name: "G(Fa & Fb)"
-  0 -> 1
+States: 3
-  1 [label="0", peripheries=2]
+Start: 0
-  1 -> 1 [label="a & b\n{0}"]
+AP: 2 "a" "b"
-  1 -> 2 [label="!b\n{0}"]
+acc-name: Buchi
-  1 -> 3 [label="!a & b\n{0}"]
+Acceptance: 1 Inf(0)
-  2 [label="1"]
+properties: trans-labels explicit-labels state-acc complete deterministic
-  2 -> 1 [label="a & b"]
+--BODY--
-  2 -> 2 [label="!b"]
+State: 0 {0}
-  2 -> 3 [label="!a & b"]
+[0&1] 0
-  3 [label="2"]
+[!1] 1
-  3 -> 1 [label="a"]
+[!0&1] 2
-  3 -> 3 [label="!a"]
+State: 1
-}
+[0&1] 0
+[!1] 1
+[!0&1] 2
+State: 2
+[0] 0
+[!0] 2
+--END--
 EOF
 
 
 cat <<EOF >expected3
-digraph G {
+HOA: v1
-  0 [label="", style=invis, height=0]
+name: "G(Fa & Fb)"
-  0 -> 1
+States: 3
-  1 [label="0", peripheries=2]
+Start: 0
-  1 -> 2 [label="1\n{0}"]
+AP: 2 "a" "b"
-  2 [label="1"]
+acc-name: Buchi
-  2 -> 2 [label="!b"]
+Acceptance: 1 Inf(0)
-  2 -> 3 [label="b"]
+properties: trans-labels explicit-labels state-acc complete deterministic
-  3 [label="2"]
+--BODY--
-  3 -> 1 [label="a"]
+State: 0 {0}
-  3 -> 3 [label="!a"]
+[t] 1
-}
+State: 1
+[!1] 1
+[1] 2
+State: 2
+[0] 0
+[!0] 2
+--END--
 EOF
 
-# FIXME: use are-isomorphic once it is available
+test -n "`../../bin/autfilt -F out2 --isomorph expected2`"
-diff out2 expected2
+test -n "`../../bin/autfilt -F out3 --isomorph expected3`"
-diff out3 expected3

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
+test -n "`../../bin/autfilt -F stdout --isomorph expected`"
-diff stdout expected
 
 rm input1 input2 stdout expected

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
+test -n "`../../bin/autfilt -F stdout --isomorph expected`"
-diff stdout expected
 rm input1 input2 stdout expected

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
+test -n "`../../bin/autfilt -F stdout --isomorph expected`"
-diff stdout expected
 
 rm input1 input2 stdout expected

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
+test -n "`../../bin/autfilt -F stdout --isomorph expected`"
-diff stdout expected
 
 rm input1 input2 stdout expected

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 <<EOF
-digraph G {
+HOA: v1
-  0 [label="", style=invis, height=0]
+States: 3
-  0 -> 1
+Start: 0
-  1 [label="0"]
+AP: 2 "p0" "p1"
-  1 -> 1 [label="1"]
+acc-name: Buchi
-  1 -> 2 [label="p0 & p1"]
+Acceptance: 1 Inf(0)
-  2 [label="1"]
+properties: trans-labels explicit-labels state-acc
-  2 -> 1 [label="!p1"]
+--BODY--
-  2 -> 2 [label="!p1"]
+State: 0
-  2 -> 3 [label="p1 & !p0"]
+[t] 0
-  3 [label="2", peripheries=2]
+[0&1] 1
-  3 -> 3 [label="1\n{0}"]
+State: 1
-}
+[!1] 0
+[!1] 1
+[!0&1] 2
+State: 2 {0}
+[t] 2
+--END--
 EOF
 
-# Sort out some possible inversions in the output.
+test -n "`../../bin/autfilt -F stdout --isomorph expected`"
-# (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
 
 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 <<EOF
-digraph G {
+HOA: v1
-  0 [label="", style=invis, height=0]
+States: 3
-  0 -> 1
+Start: 0
-  1 [label="0"]
+AP: 2 "p0" "p1"
-  1 -> 1 [label="1"]
+acc-name: Buchi
-  1 -> 2 [label="p0 & p1"]
+Acceptance: 1 Inf(0)
-  2 [label="1"]
+properties: trans-labels explicit-labels state-acc
-  2 -> 1 [label="!p1"]
+--BODY--
-  2 -> 2 [label="!p1"]
+State: 0
-  2 -> 3 [label="p1 & !p0"]
+[t] 0
-  3 [label="2", peripheries=2]
+[0&1] 1
-  3 -> 3 [label="1\n{0}"]
+State: 1
-}
+[!1] 0
+[!1] 1
+[!0&1] 2
+State: 2 {0}
+[t] 2
+--END--
 EOF
 
-# Sort out some possible inversions in the output.
+test -n "`../../bin/autfilt -F stdout --isomorph expected`"
-# (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
 
 rm input stdout expected
 

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
+test -n "`../../bin/autfilt -F input --isomorph stdout`"
-# diff input stdout
 
 # But this second output should be the same as the first
 run 0 $autfilt --hoa stdout > stdout2

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
+test -n "`../../bin/autfilt -F stdout --isomorph expected`"
-diff stdout expected
 
 rm input1 input2 input3 stdout expected