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

ltlsynt: use reduce_parity()

Browse source 
* bin/ltlsynt.cc: Here.
* tests/core/ltlsynt.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2019-06-19 23:15:02 +02:00
parent c66b3d88d0
commit c9ddbd0a73
2 changed files with 58 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

43
bin/ltlsynt.cc
View file

@ -198,7 +198,7 @@ namespace
dpa->merge_edges(); dpa->merge_edges();
if (opt_print_pg) if (opt_print_pg)
dpa = spot::sbacc(dpa); dpa = spot::sbacc(dpa);
spot::colorize_parity_here(dpa, true); spot::reduce_parity_here(dpa, true);
spot::change_parity_here(dpa, spot::parity_kind_max, spot::change_parity_here(dpa, spot::parity_kind_max,
spot::parity_style_odd); spot::parity_style_odd);
assert(( assert((
@ -317,17 +317,17 @@ namespace
{ {
auto tmp = to_dpa(aut); auto tmp = to_dpa(aut);
if (verbose) if (verbose)
std::cerr << "determinization done\n" std::cerr << "determinization done\nDPA has "
<< "dpa has " << tmp->num_states() << " states" << std::endl; << dpa->num_states() << " states, "
<< dpa->num_sets() << " colors\n";
tmp->merge_states(); tmp->merge_states();
if (verbose) if (verbose)
std::cerr << "simulation done\n" std::cerr << "simplification done\nDPA has "
<< "dpa has " << tmp->num_states() << " states" << std::endl; << tmp->num_states() << " states\n";
dpa = split_2step(tmp, all_inputs); dpa = split_2step(tmp, all_inputs);
if (verbose) if (verbose)
std::cerr << "split inputs and outputs done\n" std::cerr << "split inputs and outputs done\nautomaton has "
<< "automaton has " << dpa->num_states() << " states" << dpa->num_states() << " states\n";
<< std::endl;
spot::colorize_parity_here(dpa, true); spot::colorize_parity_here(dpa, true);
break; break;
} }
@ -335,17 +335,17 @@ namespace
{ {
auto split = split_2step(aut, all_inputs); auto split = split_2step(aut, all_inputs);
if (verbose) if (verbose)
std::cerr << "split inputs and outputs done\n" std::cerr << "split inputs and outputs done\nautomaton has "
<< "automaton has " << split->num_states() << " states" << split->num_states() << " states\n";
<< std::endl;
dpa = to_dpa(split); dpa = to_dpa(split);
if (verbose) if (verbose)
std::cerr << "determinization done\n" std::cerr << "determinization done\nDPA has "
<< "dpa has " << dpa->num_states() << " states" << std::endl; << dpa->num_states() << " states, "
<< dpa->num_sets() << " colors\n";
dpa->merge_states(); dpa->merge_states();
if (verbose) if (verbose)
std::cerr << "simulation done\n" std::cerr << "simplification done\nDPA has "
<< "dpa has " << dpa->num_states() << " states" << std::endl; << dpa->num_states() << " states\n";
break; break;
} }
case LAR: case LAR:
@ -353,17 +353,16 @@ namespace
dpa = split_2step(aut, all_inputs); dpa = split_2step(aut, all_inputs);
dpa->merge_states(); dpa->merge_states();
if (verbose) if (verbose)
std::cerr << "split inputs and outputs done\n" std::cerr << "split inputs and outputs done\nautomaton has "
<< "automaton has " << dpa->num_states() << " states" << dpa->num_states() << " states\n";
<< std::endl;
dpa = spot::to_parity(dpa); dpa = spot::to_parity(dpa);
spot::cleanup_parity_here(dpa); spot::reduce_parity_here(dpa, true);
spot::change_parity_here(dpa, spot::parity_kind_max, spot::change_parity_here(dpa, spot::parity_kind_max,
spot::parity_style_odd); spot::parity_style_odd);
if (verbose) if (verbose)
std::cerr << "LAR construction done\n" std::cerr << "LAR construction done\nDPA has "
<< "dpa has " << dpa->num_states() << " states" << std::endl; << dpa->num_states() << " states, "
spot::colorize_parity_here(dpa, true); << dpa->num_sets() << " colors\n";
break; break;
} }
} }

74
tests/core/ltlsynt.test
View file

@ -1,6 +1,6 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement # Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -23,54 +23,54 @@
set -e set -e
cat >exp <<EOF cat >exp <<EOF
parity 19; parity 17;
0 0 0 1,2 "INIT"; 0 1 0 1,2 "INIT";
2 0 1 3; 2 1 1 3;
3 2 0 4,5; 3 2 0 4,5;
5 0 1 3,6; 5 1 1 3,6;
6 3 0 4,5; 6 3 0 4,5;
4 0 1 7,8; 4 1 1 7,8;
8 0 0 9,10; 8 1 0 9,10;
10 0 1 11,12; 10 1 1 11,12;
12 0 0 9,13; 12 1 0 9,10;
13 1 1 11,12;
11 2 0 9,10;
9 3 1 3,6; 9 3 1 3,6;
7 0 0 14,15; 11 2 0 9,10;
15 1 1 7,11; 7 1 0 13,14;
14 2 1 3,6; 14 1 1 7,11;
1 0 1 3,16; 13 2 1 3,6;
16 3 0 2,17; 1 1 1 3,15;
17 3 1 3,16; 15 1 0 2,1;
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 17 1 2 1 14 aag 23 1 2 1 16
2 2
4 31 4 3
6 33 6 45
35 47
8 5 7 8 5 7
10 3 8
12 2 8 12 2 8
14 4 7 14 4 7
16 3 14 16 2 14
18 2 14
20 5 6 20 5 6
22 2 20 22 3 20
24 3 20 24 2 20
26 19 23 26 4 6
28 11 13 28 2 26
30 28 26 30 3 26
32 17 25 36 29 31
34 11 26 38 25 36
40 17 23
42 13 40
44 42 38
46 25 29
i0 a i0 a
o0 b o0 b
EOF EOF
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --aiger > out ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger >out
diff out exp diff out exp
cat >exp <<EOF cat >exp <<EOF
@ -98,7 +98,7 @@ i0 a
o0 b o0 b
o1 c o1 c
EOF EOF
ltlsynt --ins='a' --outs='b,c' -f 'GFa <-> (GFb & GFc)' --aiger > out ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger >out
diff out exp diff out exp
cat >exp <<EOF cat >exp <<EOF
@ -106,9 +106,9 @@ translating formula done
split inputs and outputs done split inputs and outputs done
automaton has 9 states automaton has 9 states
determinization done determinization done
dpa has 14 states DPA has 14 states, 4 colors
simulation done simplification done
dpa has 14 states DPA has 11 states
parity game built parity game built
EOF EOF
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out