Commit 33a94470 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

tgbatest: drop support of Spot's legacy format from ltl2tgba

This is progress for #1.

* src/tgbatest/ltl2tgba.cc: Remove options -b and -X.  Change
-P to read HOA files instead.
* src/tgbatest/complementation.cc: Replace option -b by -H for
HOA output, and read files in HOA.
* src/tgbatest/complementation.test, src/tgbatest/cycles.test,
src/tgbatest/dbacomp.test, src/tgbatest/degenid.test,
src/tgbatest/dfs.test, src/tgbatest/emptchke.test,
src/tgbatest/ltl2tgba.test, src/tgbatest/renault.test,
src/tgbatest/satmin2.test, src/tgbatest/sccsimpl.test,
src/tgbatest/sim2.test: Adjust.
parent 5852292c
......@@ -20,8 +20,8 @@
#include <iomanip>
#include <iostream>
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/save.hh"
#include "tgbaparse/public.hh"
#include "tgbaalgos/hoa.hh"
#include "hoaparse/public.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
......@@ -39,7 +39,7 @@ void usage(const char* prog)
{
std::cout << "usage: " << prog << " [options]" << std::endl;
std::cout << "with options" << std::endl
<< "-b Output in spot's format\n"
<< "-H Output in HOA\n"
<< "-s buchi_automaton display the safra automaton\n"
<< "-a buchi_automaton display the complemented automaton\n"
<< "-astat buchi_automaton statistics for !a\n"
......@@ -58,7 +58,7 @@ int main(int argc, char* argv[])
bool stats = false;
bool formula = false;
bool print_formula = false;
bool save_spot = false;
bool save_hoa = false;
if (argc < 3)
{
......@@ -70,9 +70,9 @@ int main(int argc, char* argv[])
{
if (argv[i][0] == '-')
{
if (strcmp(argv[i] + 1, "b") == 0)
if (strcmp(argv[i] + 1, "H") == 0)
{
save_spot = true;
save_hoa = true;
continue;
}
......@@ -121,10 +121,11 @@ int main(int argc, char* argv[])
if (print_automaton || print_safra)
{
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel;
spot::tgba_digraph_ptr a = spot::tgba_parse(file, pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, file, pel))
spot::hoa_parse_error_list pel;
auto h = spot::hoa_parse(file, pel, dict, env);
if (spot::format_hoa_parse_errors(std::cerr, file, pel))
return 2;
spot::tgba_digraph_ptr a = h->aut;
spot::tgba_ptr complement = 0;
......@@ -132,8 +133,8 @@ int main(int argc, char* argv[])
if (print_automaton)
{
if (save_spot)
spot::tgba_save_reachable(std::cout, complement);
if (save_hoa)
spot::hoa_reachable(std::cout, complement, nullptr);
else
spot::dotty_reachable(std::cout, complement);
}
......@@ -177,11 +178,12 @@ int main(int argc, char* argv[])
}
else
{
spot::tgba_parse_error_list pel;
spot::hoa_parse_error_list pel;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
a = spot::tgba_parse(file, pel, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, file, pel))
auto h = spot::hoa_parse(file, pel, dict, env);
if (spot::format_hoa_parse_errors(std::cerr, file, pel))
return 2;
a = h->aut;
}
auto safra_complement = spot::make_safra_complement(a);
......
......@@ -39,20 +39,31 @@ EOF
# The following test-case was supplied by Martin Dieguez Lodeiro to
# demonstrate a bug in our Safra implementation.
cat >x.tgba <<EOF
acc = "1";
"1", "1", "1",;
"1", "2", "p",;
"2", "3", "p", "1";
"2", "2", "1",;
"3", "3", "p", "1";
"3", "2", "1",;
cat >x.hoa <<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "p"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
--BODY--
State: 0
[t] 0
[0] 1
State: 1
[t] 1
[0] 2 {0}
State: 2
[t] 1
[0] 2 {0}
--END--
EOF
# x.tgba accepts some run
run 0 ../ltl2tgba -X -e x.tgba
run 0 ../ltl2tgba -XH -e x.hoa
# so does its complement
run 0 ../complement -b -a x.tgba > nx.tgba
run 0 ../ltl2tgba -X -e nx.tgba
run 0 ../complement -H -a x.hoa > nx.hoa
run 0 ../ltl2tgba -XH -e nx.hoa
# however the intersection of both should not
# accept any run.
run 0 ../ltl2tgba -X -E -Pnx.tgba x.tgba
run 1 ../../bin/autfilt -q nx.hoa --intersect x.hoa
......@@ -21,63 +21,52 @@
. ./defs
set -e
# GNU systems have seq,
# BSD systems have jot.
# Neither of those are POSIX...
if test "*`(seq 1 1 2>/dev/null)`" = "1"; then
have_seq=true
else
have_seq=false
if test "`(jot 1 1 2>/dev/null)`" = "1"; then
have_jot=true
else
have_jot=false
fi
fi
# enum start end
enum() {
if $have_seq; then
seq $1 $2
elif $have_jot; then
jot `expr $2 - $1 + 1` $1
else
i=$1
while test $i -le $2; do
echo $i
i=`expr $i + 1`
done
fi
}
# Fig.1 from Johnson's SIAM J. Comput. 1975 paper.
cat >johnson-fig1.hoa <<EOF
HOA: v1
States: 12
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[t] 1
[t] 3
[t] 4
State: 1
[t] 2
State: 2
[t] 5
[t] 6
State: 3
[t] 2
State: 4
[t] 2
State: 5
[t] 6
[t] 7
State: 6
[t] 8
[t] 10
[t] 11
State: 7
[t] 0
[t] 6
State: 8
[t] 2
[t] 9
State: 9
[t] 6
State: 10
[t] 9
State: 11
[t] 9
--END--
EOF
(
echo 'acc = ;'
k=3
v=`expr $k + 2`
w=`expr 2 \* $k + 2`
x=`expr 3 \* $k + 3`
for i in $(enum 2 `expr $k + 1`); do
echo "s1,s$i,,;"
echo "s$i,s$v,,;"
done
for i in $(enum `expr $k + 2` `expr 2 \* $k`); do
echo "s$i,s`expr $i + 1`,,;"
echo "s$i,s$w,,;"
done
echo "s`expr 2 \* $k + 1`,s$w,,;"
echo "s`expr 2 \* $k + 1`,s1,,;"
for i in $(enum `expr 2 \* $k + 3` `expr 3 \* $k + 2`); do
echo "s$w,s$i,,;"
echo "s$i,s$x,,;"
done
echo "s`expr 2 \* $k + 3`,s$v,,;"
echo "s$x,s$w,,;"
) > johnson-fig1.tgba
run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out
run 0 ../ltl2tgba -KC -XH johnson-fig1.hoa > out
test `wc -l < out` -eq 10
run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et
# Copyright (C) 2013, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -23,25 +23,37 @@ set -e
# This automaton used to trigger a bug in the complementation: its
# intersection with the complement was not empty!
cat >input.tgba <<EOF
acc = "a" "b" "c";
"1", "1", "(a & d) | (a & b)", "b" "c";
"1", "2", "a & !d & !c & !b",;
"1", "1", "(d & !a) | (b & !a)", "a" "b" "c";
"1", "2", "!a & !d & !c & !b", "a";
"2", "1", "a & c & b", "b" "c";
"2", "3", "a & b & !c", "b";
"2", "2", "a & !c & !b",;
"2", "1", "c & b & !a", "a" "b" "c";
"2", "3", "b & !a & !c", "a" "b";
"2", "2", "!a & !c & !b", "a";
"3", "1", "(a & d & c) | (a & c & b)", "b" "c";
"3", "3", "(a & d & !c) | (a & b & !c)", "b";
"3", "2", "a & !d & !c & !b",;
"3", "1", "(d & c & !a) | (c & b & !a)", "a" "b" "c";
"3", "3", "(d & !a & !c) | (b & !a & !c)", "a" "b";
"3", "2", "!a & !d & !c & !b", "a";
cat >input.hoa <<EOF
HOA: v1
States: 3
Start: 0
AP: 4 "a" "d" "b" "c"
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0&1 | 0&2] 0 {1 2}
[!0&1 | !0&2] 0 {0 1 2}
[0&!1&!2&!3] 1
[!0&!1&!2&!3] 1 {0}
State: 1
[0&2&3] 0 {1 2}
[!0&2&3] 0 {0 1 2}
[0&!2&!3] 1
[!0&!2&!3] 1 {0}
[0&2&!3] 2 {1}
[!0&2&!3] 2 {0 1}
State: 2
[0&1&3 | 0&2&3] 0 {1 2}
[!0&1&3 | !0&2&3] 0 {0 1 2}
[0&!1&!2&!3] 1
[!0&!1&!2&!3] 1 {0}
[0&1&!3 | 0&2&!3] 2 {1}
[!0&1&!3 | !0&2&!3] 2 {0 1}
--END--
EOF
# Check emptiness of product with complement.
run 0 ../ltl2tgba -Pinput.tgba -DC -E -C -X input.tgba
run 0 ../ltl2tgba -H -DC -C -XH input.hoa > output.hoa
run 1 ../../bin/autfilt -q input.hoa --intersect output.hoa
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
# Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -26,12 +26,12 @@ set -e
for f in 'FGa|GFb' 'GFa & GFb & GFc' 'GF(a->FGb)&GF(c->FGd)'; do
for opt in -DS -DT; do
../ltl2tgba $opt -b "$f" > autX.spot
../ltl2tgba -X -kt autX.spot > base.size
../ltl2tgba $opt -H "$f" > autX.spot
../ltl2tgba -XH -kt autX.spot > base.size
cat base.size
for x in X XX XXX; do
../ltl2tgba -X $opt -b aut$x.spot > autX$x.spot
../ltl2tgba -X -kt autX$x.spot > new.size
../ltl2tgba -XH $opt -H aut$x.spot > autX$x.spot
../ltl2tgba -XH -kt autX$x.spot > new.size
cat new.size
cmp base.size new.size
done
......@@ -42,61 +42,91 @@ done
# This is another 6-state degeneralized automaton that
# we used the "redegeneralize" to a 8-state BA...
cat > bug <<EOF
acc = "1";
"1", "2", "!b | !a", "1";
"1", "5", "a & b", "1";
"2", "2", "b & !a", "1";
"2", "3", "!b & !a", "1";
"2", "4", "a", "1";
"5", "1", "a & !b",;
"5", "2", "!b & !a",;
"5", "5", "a & b",;
"5", "6", "b & !a",;
"3", "1", "a & b",;
"3", "2", "b & !a",;
"3", "3", "!b & !a",;
"3", "4", "a & !b",;
"4", "1", "b",;
"4", "5", "a & !b",;
"4", "6", "!b & !a",;
"6", "1", "!b",;
"6", "3", "b & !a",;
"6", "4", "a & b",;
HOA: v1
States: 6
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] 1
[0&1] 2
State: 1 {0}
[!0&1] 1
[!0&!1] 3
[0] 4
State: 2
[0&!1] 0
[!0&!1] 1
[0&1] 2
[!0&1] 5
State: 3
[0&1] 0
[!0&1] 1
[!0&!1] 3
[0&!1] 4
State: 4
[1] 0
[0&!1] 2
[!0&!1] 5
State: 5
[!1] 0
[!0&1] 3
[0&1] 4
--END--
EOF
run 0 ../ltl2tgba -ks -X -DS bug > out
run 0 ../ltl2tgba -ks -XH -DS bug > out
grep 'states: 6' out
# This 8-state degeneralized automaton used
# to be "degeneralized" to a 9-state BA...
cat > bug2 <<EOF
acc = "1";
"1", "2", "1",;
"2", "3", "1", "1";
"3", "3", "a & !b",;
"3", "4", "a & b",;
"3", "5", "!a & !b",;
"3", "6", "b & !a",;
"4", "3", "a", "1";
"4", "5", "!a", "1";
"5", "3", "a & !b",;
"5", "4", "a & b",;
"5", "6", "b & !a",;
"5", "7", "!a & !b",;
"6", "3", "a & !b", "1";
"6", "4", "a & b", "1";
"6", "6", "b & !a", "1";
"6", "7", "!a & !b", "1";
"7", "3", "a & !b",;
"7", "4", "a & b",;
"7", "8", "b & !a",;
"7", "7", "!a & !b",;
"8", "4", "a",;
"8", "8", "!a",;
HOA: v1
States: 8
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
[t] 1
State: 1 {0}
[t] 2
State: 2
[0&!1] 2
[0&1] 3
[!0&!1] 4
[!0&1] 5
State: 3 {0}
[0] 2
[!0] 4
State: 4
[0&!1] 2
[0&1] 3
[!0&1] 5
[!0&!1] 6
State: 5 {0}
[0&!1] 2
[0&1] 3
[!0&1] 5
[!0&!1] 6
State: 6
[0&!1] 2
[0&1] 3
[!0&!1] 6
[!0&1] 7
State: 7
[0] 3
[!0] 7
--END--
EOF
run 0 ../ltl2tgba -ks -X -DS bug2 >out
run 0 ../ltl2tgba -ks -XH -DS bug2 >out
grep 'states: 8' out
......
......@@ -35,51 +35,68 @@ set -e
# |_______|
cat >blue_counter <<'EOF'
acc = a;
s1, s2,, a;
s2, s3,,;
s3, s1,,;
s3, s4,,;
s4, s4,,;
s4, s5,,;
s4, s6,,;
s4, s7,,;
s4, s8,,;
s4, s9,,;
s5, s4,,;
s5, s5,,;
s5, s6,,;
s5, s7,,;
s5, s8,,;
s5, s9,,;
s6, s4,,;
s6, s5,,;
s6, s6,,;
s6, s7,,;
s6, s8,,;
s6, s9,,;
s7, s4,,;
s7, s5,,;
s7, s6,,;
s7, s7,,;
s7, s8,,;
s7, s9,,;
s8, s4,,;
s8, s5,,;
s8, s6,,;
s8, s7,,;
s8, s8,,;
s8, s9,,;
s9, s4,,;
s9, s5,,;
s9, s6,,;
s9, s7,,;
s9, s8,,;
s9, s9,,;
HOA: v1
States: 9
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0 {0}
[t] 1
State: 1
[t] 2
State: 2
[t] 0
[t] 3
State: 3
[t] 3
[t] 4
[t] 5
[t] 6
[t] 7
[t] 8
State: 4
[t] 3
[t] 4
[t] 5
[t] 6
[t] 7
[t] 8
State: 5
[t] 3
[t] 4
[t] 5
[t] 6
[t] 7
[t] 8
State: 6
[t] 3
[t] 4
[t] 5
[t] 6
[t] 7
[t] 8
State: 7
[t] 3
[t] 4
[t] 5
[t] 6
[t] 7
[t] 8
State: 8
[t] 3
[t] 4
[t] 5
[t] 6
[t] 7
[t] 8
--END--
EOF
run 0 ../ltl2tgba -CR -eSE05 -X blue_counter
run 0 ../ltl2tgba -CR -eTau03_opt -X blue_counter
run 0 ../ltl2tgba -CR -eSE05 -XH blue_counter
run 0 ../ltl2tgba -CR -eTau03_opt -XH blue_counter
# s1->s2->s3->(large composant from s4 to s9)
# ^ ||
......@@ -87,51 +104,68 @@ run 0 ../ltl2tgba -CR -eTau03_opt -X blue_counter
# ||______||
cat >blue_last <<'EOF'
acc = a;
s1, s2,,;
s2, s3,,;
s3, s1,, a;
s3, s4,,;
s4, s4,,;
s4, s5,,;
s4, s6,,;
s4, s7,,;
s4, s8,,;
s4, s9,,;
s5, s4,,;
s5, s5,,;
s5, s6,,;
s5, s7,,;
s5, s8,,;
s5, s9,,;
s6, s4,,;
s6, s5,,;
s6, s6,,;
s6, s7,,;
s6, s8,,;
s6, s9,,;
s7, s4,,;
s7, s5,,;
s7, s6,,;
s7, s7,,;
s7, s8,,;
s7, s9,,;
s8, s4,,;
s8, s5,,;
s8, s6,,;
s8, s7,,;
s8, s8,,;
s8, s9,,;
s9, s4,,;