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

ltlsynt: Change default options

Browse source 
* bin/ltlsynt.cc: Change default options.
* tests/core/ltlsynt.test: Add test.
This commit is contained in:
Florian Renkin 2020-05-23 14:31:59 +02:00 • committed by Alexandre Duret-Lutz
parent 494471a50b
commit 0413ecfbb8
2 changed files with 92 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

3
bin/ltlsynt.cc
View file

@ -669,6 +669,9 @@ int
main(int argc, char **argv) main(int argc, char **argv)
{ {
return protected_main(argv, [&] { return protected_main(argv, [&] {
extra_options.set("simul", 0);
extra_options.set("det-simul", 0);
extra_options.set("tls-impl", 1);
const argp ap = { options, parse_opt, nullptr, const argp ap = { options, parse_opt, nullptr,
argp_program_doc, children, nullptr, nullptr }; argp_program_doc, children, nullptr, nullptr };
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))

125
tests/core/ltlsynt.test
View file

@ -23,50 +23,62 @@
set -e set -e
cat >exp <<EOF cat >exp <<EOF
parity 17; parity 18;
0 1 0 1,2 "INIT"; 0 1 0 1,2 "INIT";
2 1 1 3; 2 1 1 3;
3 2 0 4,5; 3 2 0 4,5;
5 1 1 3,6; 5 1 1 6,7;
6 3 0 4,5; 7 1 0 8,9;
4 1 1 7,8; 9 1 1 10,11;
8 1 0 9,10; 11 1 0 8,12;
10 1 1 11,12; 12 1 1 10,11;
12 1 0 9,10; 10 2 0 8,9;
9 3 1 3,6; 8 3 1 3,13;
11 2 0 9,10; 13 3 0 4,5;
7 1 0 13,14; 4 1 1 3,13;
14 1 1 7,11; 6 2 0 14,15;
13 2 1 3,6; 15 2 1 3,13;
1 1 1 3,15; 14 1 1 10,16;
15 1 0 2,1; 16 1 0 14,15;
1 1 1 3,6;
EOF EOF
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --print-pg >out ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --print-pg >out
diff out exp diff out exp
cat >exp <<EOF cat >exp <<EOF
REALIZABLE REALIZABLE
aag 23 1 2 1 16 aag 30 1 3 1 26
2 2
4 3 4 47
6 45 6 57
47 8 59
8 5 7 61
12 2 8 10 3 5
14 4 7 12 7 9
16 2 14 14 10 12
20 5 6 16 2 5
22 3 20 18 16 12
24 2 20 20 3 4
26 4 6 22 20 12
28 2 26 24 2 4
30 3 26 26 24 12
36 17 23 28 6 9
38 13 36 30 16 28
40 29 31 32 10 28
42 25 40 34 24 28
44 38 42 36 20 28
46 25 29 38 7 8
40 16 38
42 10 38
44 23 33
46 15 44
48 27 31
50 19 48
52 35 41
54 33 52
56 50 54
58 37 43
60 48 54
i0 a i0 a
o0 b o0 b
EOF EOF
@ -107,7 +119,7 @@ automaton has 3 states and 2 colors
split inputs and outputs done in X seconds split inputs and outputs done in X seconds
automaton has 9 states automaton has 9 states
determinization done determinization done
DPA has 14 states, 4 colors DPA has 12 states, 4 colors
simplification done simplification done
DPA has 11 states DPA has 11 states
determinization and simplification took X seconds determinization and simplification took X seconds
@ -124,7 +136,7 @@ automaton has 3 states and 4 colors
simplification done in X seconds simplification done in X seconds
DPA has 3 states DPA has 3 states
split inputs and outputs done in X seconds split inputs and outputs done in X seconds
automaton has 9 states automaton has 8 states
parity game built in X seconds parity game built in X seconds
parity game solved in X seconds parity game solved in X seconds
EOF EOF
@ -268,3 +280,44 @@ for i in 2 3 4 5 6 10; do
autfilt --remove-ap="$OUT" res$i | autfilt --dualize | autfilt --is-empty -q autfilt --remove-ap="$OUT" res$i | autfilt --dualize | autfilt --is-empty -q
done done
done done
cat >exp <<EOF
REALIZABLE
HOA: v1
States: 3
Start: 0
AP: 1 "p0"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[t] 1
State: 1
[t] 2
State: 2
[!0] 2
--END--
EOF
ltlsynt -x tls-impl=0 -f '!XXF(p0 & (p0 M Gp0))' > out
diff out exp
cat >exp <<EOF
REALIZABLE
HOA: v1
States: 1
Start: 0
AP: 1 "p0"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0] 0
--END--
EOF
ltlsynt -x tls-impl=1 -f '!XXF(p0 & (p0 M Gp0))' > out
diff out exp
ltlsynt -f '!XXF(p0 & (p0 M Gp0))' > out
diff out exp