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

Adapt ltlsynt

Browse source 
Using the new flexibility for solving and converting
of mealy machines and aiger circuits

* bin/ltlsynt.cc: here
This commit is contained in:
Philipp Schlehuber 2021-11-22 17:15:03 +01:00 • committed by philipp
parent 5b6e2a210a
commit 929ffc4176
1 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

17
bin/ltlsynt.cc
View file

@ -408,8 +408,14 @@ namespace
spot::mealy_like ml; spot::mealy_like ml;
ml.success = ml.success =
spot::mealy_like::realizability_code::REALIZABLE_REGULAR; spot::mealy_like::realizability_code::REALIZABLE_REGULAR;
ml.mealy_like = if (opt_print_aiger)
spot::solved_game_to_separated_mealy(arena, *gi); // we do not care about the type,
// machine to aiger can handle it
ml.mealy_like =
spot::solved_game_to_mealy(arena, *gi);
else
ml.mealy_like =
spot::solved_game_to_separated_mealy(arena, *gi);
ml.glob_cond = bddfalse; ml.glob_cond = bddfalse;
mealy_machines.push_back(ml); mealy_machines.push_back(ml);
} }
@ -452,8 +458,11 @@ namespace
delta = sw_direct.stop(); delta = sw_direct.stop();
} }
// Unsplit to have separated mealy // If our goal is to have an aiger,
m_like.mealy_like = unsplit_mealy(m_like.mealy_like); // we can use split or separated machines
if (!opt_print_aiger)
// Unsplit to have separated mealy
m_like.mealy_like = unsplit_mealy(m_like.mealy_like);
if (gi->bv) if (gi->bv)
gi->bv->strat2aut_time += delta; gi->bv->strat2aut_time += delta;