diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 6800a03f0..0d31bf67f 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -17,7 +17,14 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include + +#include +#include #include +#include +#include +#include #include #include "common_aoutput.hh" @@ -25,6 +32,7 @@ #include "common_setup.hh" #include "common_sys.hh" +#include #include #include #include @@ -42,7 +50,8 @@ enum OPT_ALGO = 256, OPT_INPUT, OPT_OUTPUT, - OPT_PRINT + OPT_PRINT, + OPT_REAL }; enum solver @@ -58,9 +67,15 @@ static const argp_option options[] = " recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial" " time algorithm)", 0 }, { "input", OPT_INPUT, "PROPS", 0, - "comma-separated list of atomic propositions", 0}, + "comma-separated list of uncontrollable (a.k.a. input) atomic" + " propositions", 0}, + { "output", OPT_OUTPUT, "PROPS", 0, + "comma-separated list of controllable (a.k.a. output) atomic" + " propositions", 0}, { "print-pg", OPT_PRINT, nullptr, 0, "print the parity game in the pgsolver format, do not solve it", 0}, + { "realizability", OPT_REAL, nullptr, 0, + "realizability only, do not synthesize the circuit", 0}, { nullptr, 0, nullptr, 0, nullptr, 0 }, }; @@ -72,10 +87,12 @@ const struct argp_child children[] = }; const char argp_program_doc[] = -"Answer the LTL realizability problem given an LTL formula and a list of" -" uncontrollable (a.k.a. input) proposition names."; +"Synthesize an AIGER circuit from its LTL specifications."; std::vector input_aps; +std::vector output_aps; +std::unordered_map bddvar_to_inputnum; +std::unordered_map bddvar_to_outputnum; bool opt_print_pg(false); bool opt_real(false); @@ -100,7 +117,7 @@ namespace // where O = AP\I, and such that cond = (i1 & o1) | (i2 & o2) | ... // // When determinized, this encodes a game automaton that has a winning - // strategy iff aut has an accepting run for all valuation of atomic + // strategy iff aut has an accepting run for any valuation of atomic // propositions in I. spot::twa_graph_ptr @@ -160,7 +177,7 @@ namespace return owner; } - spot::parity_game to_parity_game(const spot::twa_graph_ptr& split) + spot::twa_graph_ptr to_dpa(const spot::twa_graph_ptr& split) { auto dpa = spot::tgba_determinize(split); dpa->merge_edges(); @@ -174,36 +191,417 @@ namespace dpa->acc().is_parity(max, odd); assert(max && odd); assert(spot::is_deterministic(dpa)); - auto owner = make_alternating_owner(dpa); - return spot::parity_game(dpa, owner); + return dpa; + } + + // Parity game strategy to AIGER + + class aig + { + private: + unsigned num_inputs_; + unsigned max_var_; + std::map> and_gates_; + std::vector latches_; + std::vector outputs_; + // Cache the function computed by each variable as a bdd. + std::unordered_map var2bdd_; + std::unordered_map bdd2var_; + + public: + aig(unsigned num_inputs, unsigned num_latches, unsigned num_outputs) + : num_inputs_(num_inputs), + max_var_((num_inputs + num_latches) * 2), + latches_(std::vector(num_latches)), + outputs_(std::vector(num_outputs)) + { + bdd2var_[bddtrue] = 1; + var2bdd_[1] = bddtrue; + bdd2var_[bddfalse] = 0; + var2bdd_[0] = bddfalse; + } + + unsigned input_var(unsigned i, bdd b) + { + assert(i < num_inputs_); + unsigned v = (1 + i) * 2; + bdd2var_[b] = v; + var2bdd_[v] = b; + return v; + } + + unsigned latch_var(unsigned i, bdd b) + { + assert(i < latches_.size()); + unsigned v = (1 + num_inputs_ + i) * 2; + bdd2var_[b] = v; + var2bdd_[v] = b; + return v; + } + + void set_output(unsigned i, unsigned v) + { + outputs_[i] = v; + } + + void set_latch(unsigned i, unsigned v) + { + latches_[i] = v; + } + + unsigned aig_true() const + { + return 1; + } + + unsigned aig_false() const + { + return 0; + } + + unsigned aig_not(unsigned v) + { + unsigned not_v = v + 1 - 2 * (v % 2); + assert(var2bdd_.count(v)); + var2bdd_[not_v] = !(var2bdd_[v]); + bdd2var_[var2bdd_[not_v]] = not_v; + return not_v; + } + + unsigned aig_and(unsigned v1, unsigned v2) + { + assert(var2bdd_.count(v1)); + assert(var2bdd_.count(v2)); + bdd b = var2bdd_[v1] & var2bdd_[v2]; + auto it = bdd2var_.find(b); + if (it != bdd2var_.end()) + return it->second; + max_var_ += 2; + and_gates_[max_var_] = {v1, v2}; + bdd v1v2 = var2bdd_[v1] & var2bdd_[v2]; + bdd2var_[v1v2] = max_var_; + var2bdd_[max_var_] = v1v2; + return max_var_; + } + + unsigned aig_and(std::vector vs) + { + if (vs.empty()) + return aig_true(); + if (vs.size() == 1) + return vs[0]; + if (vs.size() == 2) + return aig_and(vs[0], vs[1]); + unsigned m = vs.size() / 2; + std::vector left(vs.begin(), vs.begin() + m); + std::vector right(vs.begin() + m, vs.end()); + return aig_and(aig_and(left), aig_and(right)); + } + + unsigned aig_or(unsigned v1, unsigned v2) + { + return aig_not(aig_and(aig_not(v1), aig_not(v2))); + } + + unsigned aig_or(std::vector vs) + { + for (unsigned i = 0; i < vs.size(); ++i) + vs[i] = aig_not(vs[i]); + return aig_not(aig_and(vs)); + } + + unsigned aig_pos(unsigned v) + { + return v - v % 2; + } + + void remove_unused() + { + std::unordered_set todo; + for (unsigned v : outputs_) + todo.insert(aig_pos(v)); + std::unordered_set used; + while (!todo.empty()) + { + used.insert(todo.begin(), todo.end()); + std::unordered_set todo_next; + for (unsigned v : todo) + { + auto it_and = and_gates_.find(v); + if (it_and != and_gates_.end()) + { + if (!used.count(aig_pos(it_and->second.first))) + todo_next.insert(aig_pos(it_and->second.first)); + if (!used.count(aig_pos(it_and->second.second))) + todo_next.insert(aig_pos(it_and->second.second)); + } + else if (v <= (num_inputs_ + latches_.size()) * 2 + && v > num_inputs_ * 2) + { + unsigned l = v / 2 - num_inputs_ - 1; + if (!used.count(aig_pos(latches_[l]))) + todo_next.insert(aig_pos(latches_[l])); + } + } + todo = todo_next; + } + std::unordered_set unused; + for (auto& p : and_gates_) + if (!used.count(p.first)) + unused.insert(p.first); + for (unsigned v : unused) + and_gates_.erase(v); + } + + void print() + { + std::cout << "aag " << max_var_ / 2 + << ' ' << num_inputs_ + << ' ' << latches_.size() + << ' ' << outputs_.size() + << ' ' << and_gates_.size() << '\n'; + for (unsigned i = 0; i < num_inputs_; ++i) + std::cout << (1 + i) * 2 << '\n'; + for (unsigned i = 0; i < latches_.size(); ++i) + std::cout << (1 + num_inputs_ + i) * 2 + << ' ' << latches_[i] << '\n'; + for (unsigned i = 0; i < outputs_.size(); ++i) + std::cout << outputs_[i] << '\n'; + for (auto& p : and_gates_) + std::cout << p.first + << ' ' << p.second.first + << ' ' << p.second.second << '\n'; + for (unsigned i = 0; i < num_inputs_; ++i) + std::cout << 'i' << i << ' ' << input_aps[i] << '\n'; + for (unsigned i = 0; i < outputs_.size(); ++i) + std::cout << 'o' << i << ' ' << output_aps[i] << '\n'; + } + }; + + std::vector output_to_vec(bdd b) + { + std::vector v(bddvar_to_outputnum.size()); + while (b != bddtrue && b != bddfalse) + { + unsigned i = bddvar_to_outputnum[bdd_var(b)]; + v[i] = (bdd_low(b) == bddfalse); + if (v[i]) + b = bdd_high(b); + else + b = bdd_low(b); + } + return v; + } + + bdd state_to_bdd(unsigned s, bdd all) + { + bdd b = bddtrue; + unsigned size = bdd_nodecount(all); + if (size) + { + unsigned st0 = bdd_var(all); + for (unsigned i = 0; i < size; ++i) + { + b &= s % 2 ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i); + s >>= 1; + } + } + return b; + } + + // Construct a smaller automaton, filtering out states that are not + // accessible. Also merge back pairs of p --(i)--> q --(o)--> r + // transitions to p --(i&o)--> r. + spot::twa_graph_ptr + strat_to_aut(const spot::parity_game& pg, + const spot::parity_game::strategy_t& strat, + const spot::twa_graph_ptr& dpa, + bdd all_outputs) + { + auto aut = spot::make_twa_graph(dpa->get_dict()); + aut->copy_ap_of(dpa); + std::vector todo{pg.get_init_state_number()}; + std::vector pg2aut(pg.num_states(), -1); + aut->set_init_state(aut->new_state()); + pg2aut[pg.get_init_state_number()] = aut->get_init_state_number(); + while (!todo.empty()) + { + unsigned s = todo.back(); + todo.pop_back(); + for (auto& e1: dpa->out(s)) + { + unsigned i = 0; + for (auto& e2: dpa->out(e1.dst)) + { + bool self_loop = false; + if (e1.dst == s || e2.dst == e1.dst) + self_loop = true; + if (self_loop || strat.at(e1.dst) == i) + { + bdd out = bdd_satoneset(e2.cond, all_outputs, bddfalse); + if (pg2aut[e2.dst] == -1) + { + pg2aut[e2.dst] = aut->new_state(); + todo.push_back(e2.dst); + } + aut->new_edge(pg2aut[s], pg2aut[e2.dst], + (e1.cond & out), 0); + break; + } + ++i; + } + } + } + aut->purge_dead_states(); + return aut; + } + + std::vector state_to_vec(unsigned s, unsigned size) + { + std::vector v(size); + for (unsigned i = 0; i < size; ++i) + { + v[i] = s % 2; + s >>= 1; + } + return v; + } + + // Switch initial state and 0 in the AIGER encoding, so that the + // 0-initialized latches correspond to the initial state. + unsigned encode_init_0(unsigned src, unsigned init) + { + return src == init ? 0 : src == 0 ? init : src; + } + + aig aut_to_aiger(const spot::twa_graph_ptr& aut, + bdd all_inputs, bdd all_outputs) + { + // Encode state in log2(num_states) latches. + unsigned log2n = std::ceil(std::log2(aut->num_states())); + unsigned st0 = aut->get_dict()->register_anonymous_variables(log2n, aut); + bdd all_states = bddtrue; + for (unsigned i = 0; i < log2n; ++i) + all_states &= bdd_ithvar(st0 + i); + + unsigned num_inputs = bdd_nodecount(all_inputs); + unsigned num_outputs = bdd_nodecount(all_outputs); + unsigned num_latches = bdd_nodecount(all_states); + unsigned init = aut->get_init_state_number(); + + aig circuit(num_inputs, num_latches, num_outputs); + bdd b; + + // Latches and outputs are expressed as a DNF in which each term represents + // a transition. + // latch[i] (resp. out[i]) represents the i-th latch's (resp. output's) + // DNF. + std::vector> latch(num_latches); + std::vector> out(num_outputs); + for (unsigned s = 0; s < aut->num_states(); ++s) + for (auto& e: aut->out(s)) + { + spot::minato_isop cond(e.cond); + while ((b = cond.next()) != bddfalse) + { + bdd input = bdd_existcomp(b, all_inputs); + bdd letter_out = bdd_existcomp(b, all_outputs); + auto out_vec = output_to_vec(letter_out); + unsigned dst = encode_init_0(e.dst, init); + auto next_state_vec = state_to_vec(dst, log2n); + unsigned src = encode_init_0(s, init); + bdd state_bdd = state_to_bdd(src, all_states); + std::vector prod; + while (input != bddfalse && input != bddtrue) + { + unsigned v = + circuit.input_var(bddvar_to_inputnum[bdd_var(input)], + bdd_ithvar(bdd_var(input))); + if (bdd_high(input) == bddfalse) + { + v = circuit.aig_not(v); + input = bdd_low(input); + } + else + input = bdd_high(input); + prod.push_back(v); + } + + while (state_bdd != bddfalse && state_bdd != bddtrue) + { + unsigned v = + circuit.latch_var(bdd_var(state_bdd) - st0, + bdd_ithvar(bdd_var(state_bdd))); + if (bdd_high(state_bdd) == bddfalse) + { + v = circuit.aig_not(v); + state_bdd = bdd_low(state_bdd); + } + else + state_bdd = bdd_high(state_bdd); + prod.push_back(v); + } + unsigned t = circuit.aig_and(prod); + for (unsigned i = 0; i < next_state_vec.size(); ++i) + if (next_state_vec[i]) + latch[i].push_back(t); + for (unsigned i = 0; i < num_outputs; ++i) + if (out_vec[i]) + out[i].push_back(t); + } + } + for (unsigned i = 0; i < num_latches; ++i) + circuit.set_latch(i, circuit.aig_or(latch[i])); + for (unsigned i = 0; i < num_outputs; ++i) + circuit.set_output(i, circuit.aig_or(out[i])); + circuit.remove_unused(); + return circuit; } class ltl_processor final : public job_processor { - public: - spot::translator& trans; - std::vector input_aps; + private: + spot::translator& trans_; + std::vector input_aps_; + std::vector output_aps_; - ltl_processor(spot::translator& trans, std::vector input_aps) - : trans(trans), input_aps(input_aps) + public: + + ltl_processor(spot::translator& trans, + std::vector input_aps_, + std::vector output_aps_) + : trans_(trans), input_aps_(input_aps_), output_aps_(output_aps_) { } int process_formula(spot::formula f, const char*, int) override { - auto aut = trans.run(&f); - bdd input_bdd = bddtrue; - for (unsigned i = 0; i < input_aps.size(); ++i) + auto aut = trans_.run(&f); + bdd all_inputs = bddtrue; + bdd all_outputs = bddtrue; + for (unsigned i = 0; i < input_aps_.size(); ++i) { std::ostringstream lowercase; - for (char c: input_aps[i]) + for (char c: input_aps_[i]) lowercase << (char)std::tolower(c); - auto ap = spot::formula::ap(lowercase.str()); - input_bdd &= bdd_ithvar(aut->register_ap(ap)); + unsigned v = aut->register_ap(spot::formula::ap(lowercase.str())); + all_inputs &= bdd_ithvar(v); + bddvar_to_inputnum[v] = i; } - auto split = split_automaton(aut, input_bdd); - auto pg = to_parity_game(split); + for (unsigned i = 0; i < output_aps_.size(); ++i) + { + std::ostringstream lowercase; + for (char c: output_aps_[i]) + lowercase << (char)std::tolower(c); + unsigned v = aut->register_ap(spot::formula::ap(lowercase.str())); + all_outputs &= bdd_ithvar(v); + bddvar_to_outputnum[v] = i; + } + auto split = split_automaton(aut, all_inputs); + auto dpa = to_dpa(split); + auto owner = make_alternating_owner(dpa); + auto pg = spot::parity_game(dpa, owner); if (opt_print_pg) { pg.print(std::cout); @@ -213,14 +611,31 @@ namespace { case REC: { - if (std::get<0>(pg.solve()).count(pg.get_init_state_number())) - std::cout << "REALIZABLE\n"; + spot::parity_game::strategy_t strategy; + spot::parity_game::region_t winning_region; + std::tie(winning_region, strategy) = pg.solve(); + if (winning_region.count(pg.get_init_state_number())) + { + std::cout << "REALIZABLE\n"; + if (!opt_real) + { + auto strat_aut = strat_to_aut(pg, strategy, dpa, all_outputs); + auto circuit = aut_to_aiger(strat_aut, all_inputs, all_outputs); + circuit.print(); + } + } else std::cout << "UNREALIZABLE\n"; return 0; } case QP: - if (pg.solve_qp()) + if (!opt_real) + { + std::cout << "The quasi-polynomial time algorithm does not" + " implement synthesis yet, use --realizability\n"; + return 1; + } + else if (pg.solve_qp()) std::cout << "REALIZABLE\n"; else std::cout << "UNREALIZABLE\n"; @@ -249,6 +664,17 @@ parse_opt(int key, char* arg, struct argp_state*) } break; } + case OPT_OUTPUT: + { + std::istringstream aps(arg); + std::string ap; + while (std::getline(aps, ap, ',')) + { + ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); + output_aps.push_back(ap); + } + break; + } case OPT_PRINT: opt_print_pg = true; break; @@ -263,6 +689,9 @@ parse_opt(int key, char* arg, struct argp_state*) return 1; } break; + case OPT_REAL: + opt_real = true; + break; } return 0; } @@ -277,6 +706,6 @@ int main(int argc, char **argv) check_no_formula(); spot::translator trans; - ltl_processor processor(trans, input_aps); + ltl_processor processor(trans, input_aps, output_aps); processor.run(); } diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index a7e6e31ee..b4c043ad8 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -6,14 +6,41 @@ * Basic usage -This tool answers whether a controller can be built given an LTL/PSL formula -specifying its behavior. =ltlsynt= is typically called with -the following three options: +This tool synthesizes [[http://fmv.jku.at/aiger/][AIGER]] circuits from LTL/PSL +formulas. =ltlsynt= is typically called with the following three options: - =--input=: a comma-separated list of input signal names - =--output=: a comma-separated list of output signal names - =--formula= or =--file=: the LTL/PSL specification. +The following example illustrates the synthesis of an =AND= gate. We call the two +inputs =a= and =b=, and the output =c=. We want the relationship between the +inputs and the output to always hold, so we prefix the propositional formula +with a =G= operator: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlsynt --input=a,b --output=c --formula 'G (a & b <=> c)' +#+END_SRC + +#+RESULTS: +#+begin_example +REALIZABLE +aag 3 2 0 1 1 +2 +4 +6 +6 2 4 +i0 a +i1 b +o0 c +#+end_example + +The output is composed of two sections. The first one is a single line +containing either REALIZABLE or UNREALIZABLE, and the second one is an AIGER +circuit that satisfies the specification (or nothing if it is unrealizable). +In this example, the generated circuit contains, as expected, a single =AND= +gate linking the two inputs to the output. + The following example is unrealizable, because =a= is an input, so no circuit can guarantee that it will be true eventually. @@ -35,7 +62,7 @@ Fortunately, the SYNTCOMP organizers also provide a tool called =syfco= which can translate a TLSF specification to an LTL formula. The following four steps show you how a TLSF specification called spec.tlsf can -be tested for realizability using =syfco= and =ltlsynt=: +be synthesized using =syfco= and =ltlsynt=: #+BEGIN_SRC sh LTL=$(syfco FILE -f ltlxba -m fully) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test new file mode 100644 index 000000000..0d9cfdd51 --- /dev/null +++ b/tests/core/ltlsynt.test @@ -0,0 +1,1090 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs || exit 1 + +set -e + +F0='(G ((((req) -> (X ((grant) && (X ((grant) && (X (grant))))))) && ((grant) +-> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))' +IN0='cancel, go, req' +OUT0='grant' +EXP0='UNREALIZABLE' +F1='(G ((((req) -> (X ((grant) || (X ((grant) || (X (grant))))))) && ((grant) +-> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))' +IN1='cancel, go, req' +OUT1='grant' +EXP1='UNREALIZABLE' +F2='((G ((cancel) -> (X (go)))) -> (G ((((req) -> (X ((grant) || (X ((grant) || +(X (grant))))))) && ((grant) -> (X (! (grant))))) && ((cancel) -> (X ((! +(grant)) U (go)))))))' +IN2='cancel, go, req' +OUT2='grant' +EXP2='REALIZABLE' +F3='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((req) -> (X ((grant) || +(X ((grant) || (X (grant))))))) && ((grant) -> (X (! (grant))))) && ((cancel) +-> (X ((! (grant)) U (go)))))))' +IN3='cancel, go, req' +OUT3='grant' +EXP3='REALIZABLE' +F4='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((req) -> (X (((grant) || +(cancel)) || (X (((grant) || (cancel)) || (X ((grant) || (cancel)))))))) && +((grant) -> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go)))))))' +IN4='cancel, go, req' +OUT4='grant' +EXP4='REALIZABLE' +F5='((G ((cancel) -> (X ((go) || (X ((go) || (X (go)))))))) -> (G ((((req) -> +(X (((grant) || (cancel)) || (X (((grant) || (cancel)) || (X ((grant) || +(cancel)))))))) && ((grant) -> (X (! (grant))))) && ((cancel) -> (X ((! +(grant)) U (go)))))))' +IN5='cancel, go, req' +OUT5='grant' +EXP5='REALIZABLE' +F6='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((cancel) -> (X ((! +(grant)) U (go)))) && ((grant) -> (X (! (grant))))) && ((req) -> (((grant) || +(cancel)) || (X (((grant) || (cancel)) || (X (((grant) || (cancel)) || (X +((grant) || (cancel))))))))))))' +IN6='cancel, go, req' +OUT6='grant' +EXP6='REALIZABLE' +F7='(! ((G ((req) -> (F (ack)))) && (G ((go) -> (F (grant))))))' +IN7='go, req' +OUT7='ack, grant' +EXP7='UNREALIZABLE' +F8='(((G ((((r1) -> (F (a1))) && ((r2) -> (F (a2)))) && (! ((a1) && (a2))))) && +(((a1) U (r1)) || (G (a1)))) && (((a2) U (r2)) || (G (a2))))' +IN8='r1, r2' +OUT8='a1, a2' +EXP8='UNREALIZABLE' +F9='((((G (((((((r0) -> (F (a0))) && ((r1) -> (F (a1)))) && ((r2) -> (F (a2)))) +&& (! ((a0) && (a1)))) && (! ((a0) && (a2)))) && (! ((a1) && (a2))))) && (((a0) +U (r0)) || (G (a0)))) && (((a1) U (r1)) || (G (a1)))) && (((a2) U (r2)) || (G +(a2))))' +IN9='r0, r1, r2' +OUT9='a0, a1, a2' +EXP9='UNREALIZABLE' + +cat <exp2 +REALIZABLE +aag 144 3 4 1 132 +2 +4 +6 +8 211 +10 245 +12 271 +14 289 +271 +16 13 15 +18 11 16 +20 3 9 +26 6 20 +28 26 18 +30 2 9 +32 7 30 +34 32 18 +36 6 30 +38 36 18 +40 3 8 +42 7 40 +44 42 18 +46 6 40 +48 46 18 +50 2 8 +52 7 50 +54 52 18 +56 6 50 +58 56 18 +60 9 10 +62 60 16 +64 3 4 +66 7 64 +70 6 64 +72 70 62 +74 2 4 +76 7 74 +78 76 62 +80 6 74 +82 80 62 +84 10 16 +86 5 9 +88 86 84 +90 8 10 +92 90 16 +94 66 92 +96 70 92 +98 76 92 +100 80 92 +102 5 8 +104 102 84 +106 12 15 +108 11 106 +112 26 108 +114 32 108 +116 36 108 +118 40 108 +120 50 108 +122 60 106 +126 70 122 +128 76 122 +130 80 122 +132 10 106 +134 86 132 +136 4 8 +138 3 136 +140 138 132 +142 2 136 +144 142 132 +146 102 132 +148 13 14 +150 9 11 +152 150 148 +154 11 148 +156 42 154 +158 46 154 +160 52 154 +162 56 154 +164 10 148 +166 86 164 +168 60 148 +170 66 168 +172 70 168 +174 76 168 +176 80 168 +178 173 177 +180 163 178 +182 141 159 +184 182 180 +186 127 131 +188 117 119 +190 188 186 +192 190 184 +194 101 113 +196 97 194 +198 73 83 +200 198 196 +202 49 59 +204 29 39 +206 204 202 +208 206 200 +210 208 192 +212 175 177 +214 163 212 +216 145 161 +218 216 214 +220 129 131 +222 117 121 +224 222 220 +226 224 218 +228 101 115 +230 99 228 +232 79 83 +234 232 230 +236 55 59 +238 35 39 +240 238 236 +242 240 234 +244 242 226 +246 171 173 +248 246 212 +250 161 163 +252 157 159 +254 252 250 +256 254 248 +258 99 101 +260 95 97 +262 260 258 +264 45 49 +266 264 236 +268 266 262 +270 268 256 +272 153 167 +274 147 272 +276 141 145 +278 276 274 +280 121 135 +282 119 280 +284 89 105 +286 284 282 +288 286 278 +i0 cancel +i1 go +i2 req +o0 grant +EOF + +cat <exp3 +REALIZABLE +aag 264 3 4 1 257 +2 +4 +6 +8 313 +10 377 +12 443 +14 483 +529 +16 13 15 +18 11 16 +20 3 9 +22 7 20 +24 22 18 +26 2 9 +28 7 26 +30 28 18 +32 6 26 +34 32 18 +36 6 20 +38 36 18 +40 3 8 +42 7 40 +44 42 18 +46 2 8 +48 7 46 +50 48 18 +52 6 46 +54 52 18 +56 6 40 +58 56 18 +60 9 10 +62 60 16 +64 3 4 +66 7 64 +68 66 62 +70 2 4 +72 7 70 +74 72 62 +76 6 70 +78 76 62 +80 6 64 +82 80 62 +84 10 16 +86 5 9 +88 7 86 +90 88 84 +92 6 86 +94 92 84 +96 5 8 +98 96 84 +100 8 10 +102 100 16 +104 66 102 +106 72 102 +108 76 102 +110 80 102 +112 12 15 +114 11 112 +116 22 114 +118 28 114 +120 32 114 +122 36 114 +124 42 114 +126 48 114 +128 52 114 +130 56 114 +132 60 112 +134 66 132 +136 72 132 +138 76 132 +140 80 132 +142 10 112 +144 88 142 +146 92 142 +148 96 142 +150 4 8 +152 3 150 +154 152 142 +156 2 150 +158 156 142 +160 13 14 +162 11 160 +164 20 162 +166 26 162 +168 42 162 +170 48 162 +172 52 162 +174 56 162 +176 60 160 +178 66 176 +180 72 176 +182 76 176 +184 80 176 +186 10 160 +188 86 186 +190 96 186 +192 100 160 +194 66 192 +196 72 192 +198 76 192 +200 80 192 +202 12 14 +204 9 11 +206 204 202 +208 11 202 +210 96 208 +212 8 11 +214 212 202 +216 66 214 +218 72 214 +220 76 214 +222 80 214 +224 60 202 +226 66 224 +228 72 224 +230 76 224 +232 80 224 +234 10 202 +236 86 234 +238 100 202 +240 66 238 +242 72 238 +244 76 238 +246 80 238 +248 96 234 +250 241 245 +252 231 250 +254 221 227 +256 254 252 +258 199 217 +260 189 195 +262 260 258 +264 262 256 +266 179 183 +268 169 173 +270 268 266 +272 155 165 +274 147 149 +276 274 272 +278 276 270 +280 278 264 +282 135 139 +284 125 129 +286 284 282 +288 117 121 +290 105 109 +292 290 288 +294 292 286 +296 95 99 +298 69 79 +300 298 296 +302 45 55 +304 25 35 +306 304 302 +308 306 300 +310 308 294 +312 310 280 +314 243 245 +316 231 314 +318 221 229 +320 318 316 +322 199 219 +324 189 197 +326 324 322 +328 326 320 +330 181 183 +332 171 173 +334 332 330 +336 159 167 +338 145 147 +340 338 336 +342 340 334 +344 342 328 +346 137 139 +348 127 129 +350 348 346 +352 119 121 +354 107 109 +356 354 352 +358 356 350 +360 91 95 +362 75 79 +364 362 360 +366 51 55 +368 31 35 +370 368 366 +372 370 364 +374 372 358 +376 374 344 +378 245 249 +380 243 378 +382 237 241 +384 382 380 +386 221 233 +388 219 386 +390 211 217 +392 390 388 +394 392 384 +396 199 207 +398 197 396 +400 191 195 +402 400 398 +404 173 179 +406 404 330 +408 406 402 +410 408 394 +412 169 171 +414 149 412 +416 338 414 +418 131 141 +420 121 418 +422 117 119 +424 422 420 +426 424 416 +428 105 354 +430 296 428 +432 83 91 +434 39 59 +436 434 432 +438 436 430 +440 438 426 +442 440 410 +444 247 249 +446 237 444 +448 211 223 +450 207 448 +452 450 446 +454 191 201 +456 189 454 +458 175 185 +460 167 458 +462 460 456 +464 462 452 +466 159 165 +468 155 466 +470 145 274 +472 470 468 +474 111 123 +476 99 474 +478 360 476 +480 478 472 +482 480 464 +484 245 247 +486 241 243 +488 486 484 +490 221 223 +492 219 490 +494 492 488 +496 201 217 +498 197 199 +500 498 496 +502 185 195 +504 183 502 +506 504 500 +508 506 494 +510 179 181 +512 173 175 +514 512 510 +516 123 412 +518 516 514 +520 111 117 +522 520 352 +524 428 522 +526 524 518 +528 526 508 +i0 cancel +i1 go +i2 req +o0 grant +EOF + +cat <exp4 +REALIZABLE +aag 174 3 4 1 163 +2 +4 +6 +8 251 +10 299 +12 325 +14 333 +349 +16 13 15 +18 11 16 +20 7 9 +22 3 20 +26 6 9 +28 3 26 +30 28 18 +32 2 20 +34 32 18 +36 2 26 +38 36 18 +40 7 8 +42 2 40 +44 42 18 +46 6 8 +48 2 46 +50 48 18 +52 3 40 +54 52 18 +56 3 46 +58 56 18 +60 9 10 +62 60 16 +64 7 4 +66 3 64 +70 6 4 +72 3 70 +74 72 62 +76 2 64 +78 76 62 +80 2 70 +82 80 62 +84 10 16 +86 5 9 +88 7 86 +90 88 84 +92 6 86 +94 92 84 +96 8 10 +98 96 16 +100 76 98 +102 80 98 +104 66 98 +106 72 98 +108 7 5 +110 2 108 +112 110 98 +114 6 5 +116 2 114 +118 116 98 +120 5 8 +122 3 120 +124 122 84 +126 12 15 +128 11 126 +132 28 128 +134 32 128 +136 36 128 +138 42 128 +140 48 128 +142 3 8 +144 142 128 +146 60 126 +150 72 146 +152 76 146 +154 80 146 +156 10 126 +158 86 156 +160 96 126 +162 76 160 +164 80 160 +166 66 160 +168 72 160 +170 120 156 +172 13 14 +174 9 11 +176 174 172 +178 76 176 +180 80 176 +182 66 176 +184 72 176 +186 11 172 +188 86 186 +190 8 11 +192 190 172 +194 10 172 +196 32 194 +198 36 194 +200 22 194 +202 28 194 +204 199 203 +206 189 193 +208 206 204 +210 181 185 +212 171 210 +214 212 208 +216 165 169 +218 159 216 +220 151 155 +222 141 220 +224 222 218 +226 224 214 +228 133 137 +230 119 228 +232 103 107 +234 95 232 +236 234 230 +238 75 83 +240 59 238 +242 39 51 +244 31 242 +246 244 240 +248 246 236 +250 248 226 +252 197 199 +254 179 181 +256 254 252 +258 163 165 +260 155 258 +262 260 256 +264 145 153 +266 141 264 +268 137 139 +270 135 268 +272 270 266 +274 272 262 +276 113 119 +278 103 276 +280 95 101 +282 91 280 +284 282 278 +286 79 83 +288 51 286 +290 39 45 +292 35 290 +294 292 288 +296 294 284 +298 296 274 +300 201 203 +302 183 185 +304 302 300 +306 167 169 +308 119 306 +310 308 304 +312 107 113 +314 95 105 +316 314 312 +318 59 91 +320 55 318 +322 320 316 +324 322 310 +326 171 206 +328 145 159 +330 125 328 +332 330 326 +334 185 300 +336 169 183 +338 336 334 +340 107 167 +342 105 340 +344 55 59 +346 344 342 +348 346 338 +i0 cancel +i1 go +i2 req +o0 grant +EOF + +cat <exp5 +REALIZABLE +aag 289 3 4 1 282 +2 +4 +6 +8 367 +10 455 +12 509 +14 547 +579 +16 13 15 +18 11 16 +20 7 9 +22 3 20 +24 22 18 +26 2 20 +28 26 18 +30 6 9 +32 2 30 +34 32 18 +36 3 30 +38 36 18 +40 7 8 +42 3 40 +44 42 18 +46 2 40 +48 46 18 +50 6 8 +52 2 50 +54 52 18 +56 3 50 +58 56 18 +60 9 10 +62 60 16 +64 7 4 +66 3 64 +68 66 62 +70 2 64 +72 70 62 +74 6 4 +76 2 74 +78 76 62 +80 3 74 +82 80 62 +84 10 16 +86 5 9 +88 7 86 +90 88 84 +92 6 86 +94 92 84 +96 8 10 +98 96 16 +100 70 98 +102 76 98 +104 7 5 +106 2 104 +108 106 98 +110 6 5 +112 2 110 +114 112 98 +116 5 8 +118 3 116 +120 118 84 +122 66 98 +124 80 98 +126 12 15 +128 11 126 +130 26 128 +132 32 128 +134 22 128 +136 36 128 +138 46 128 +140 52 128 +142 3 8 +144 142 128 +146 10 126 +148 26 146 +150 32 146 +152 22 146 +154 36 146 +156 96 126 +158 66 156 +160 70 156 +162 76 156 +164 80 156 +166 7 116 +168 166 146 +170 6 116 +172 170 146 +174 13 14 +176 9 11 +178 176 174 +180 70 178 +182 76 178 +184 66 178 +186 80 178 +188 106 178 +190 112 178 +192 11 174 +194 3 86 +196 194 192 +198 8 11 +200 198 174 +202 70 200 +204 76 200 +206 106 200 +208 112 200 +210 118 192 +212 66 200 +214 80 200 +216 60 174 +218 66 216 +220 70 216 +222 76 216 +224 80 216 +226 10 174 +228 86 226 +230 96 174 +232 70 230 +234 76 230 +236 66 230 +238 80 230 +240 116 226 +242 12 14 +244 176 242 +246 70 244 +248 76 244 +250 11 242 +252 86 250 +254 66 244 +256 80 244 +258 198 242 +260 10 242 +262 22 260 +264 26 260 +266 32 260 +268 36 260 +270 96 242 +272 70 270 +274 76 270 +276 66 270 +278 80 270 +280 116 260 +282 279 281 +284 277 282 +286 267 275 +288 259 286 +290 288 284 +292 255 257 +294 253 292 +296 241 249 +298 296 294 +300 298 290 +302 237 239 +304 235 302 +306 223 229 +308 215 306 +310 308 304 +312 209 213 +314 205 312 +316 191 197 +318 316 314 +320 318 310 +322 320 300 +324 185 187 +326 183 324 +328 163 173 +330 155 328 +332 330 326 +334 151 153 +336 141 334 +338 135 137 +340 338 336 +342 340 332 +344 125 133 +346 123 344 +348 109 121 +350 103 348 +352 350 346 +354 79 91 +356 55 354 +358 25 35 +360 358 356 +362 360 352 +364 362 342 +366 364 322 +368 273 275 +370 267 368 +372 263 265 +374 249 372 +376 374 370 +378 235 247 +380 233 378 +382 221 223 +384 219 382 +386 384 380 +388 386 376 +390 207 209 +392 205 390 +394 197 203 +396 191 394 +398 396 392 +400 183 189 +402 181 400 +404 169 173 +406 404 402 +408 406 398 +410 408 388 +412 161 163 +414 159 412 +416 149 151 +418 145 416 +420 418 414 +422 139 141 +424 133 422 +426 109 131 +428 426 424 +430 428 420 +432 101 103 +434 91 432 +436 73 79 +438 69 436 +440 438 434 +442 49 55 +444 45 442 +446 29 35 +448 446 444 +450 448 440 +452 450 430 +454 452 410 +456 263 269 +458 456 282 +460 257 259 +462 241 253 +464 462 460 +466 464 458 +468 229 239 +470 219 225 +472 470 468 +474 211 215 +476 197 474 +478 476 472 +480 478 466 +482 165 187 +484 155 159 +486 484 482 +488 137 145 +490 125 488 +492 490 486 +494 91 109 +496 69 83 +498 496 494 +500 45 59 +502 39 500 +504 502 498 +506 504 492 +508 506 480 +510 263 281 +512 259 510 +514 229 462 +516 514 512 +518 211 219 +520 209 518 +522 197 207 +524 522 520 +526 524 516 +528 189 191 +530 173 528 +532 159 169 +534 532 530 +536 115 121 +538 95 536 +540 45 69 +542 540 538 +544 542 534 +546 544 526 +548 277 279 +550 257 548 +552 239 255 +554 552 550 +556 215 237 +558 187 213 +560 558 556 +562 560 554 +564 155 185 +566 137 153 +568 566 564 +570 125 135 +572 25 123 +574 572 570 +576 574 568 +578 576 562 +i0 cancel +i1 go +i2 req +o0 grant +EOF + +cat <exp6 +REALIZABLE +aag 76 3 3 1 63 +2 +4 +6 +8 125 +10 141 +12 147 +153 +14 11 13 +16 2 9 +18 16 14 +20 9 14 +26 3 6 +28 26 20 +30 8 14 +32 2 4 +34 32 30 +42 6 4 +44 3 42 +46 44 30 +48 6 5 +50 3 48 +52 50 30 +54 2 5 +56 54 30 +58 7 5 +60 58 30 +62 10 13 +64 16 62 +66 9 62 +70 26 66 +72 2 8 +74 72 62 +76 3 8 +78 76 62 +80 11 12 +82 9 80 +84 32 82 +86 3 4 +88 86 82 +90 5 9 +92 90 80 +94 8 80 +96 32 94 +100 44 94 +102 5 8 +104 102 80 +106 10 12 +108 9 106 +110 85 97 +112 75 110 +114 65 71 +116 114 112 +118 57 61 +120 19 35 +122 120 118 +124 122 116 +126 105 109 +128 101 126 +130 89 93 +132 130 128 +134 71 79 +136 29 47 +138 136 134 +140 138 132 +142 93 126 +144 53 118 +146 144 142 +148 89 101 +150 79 148 +152 136 150 +i0 cancel +i1 go +i2 req +o0 grant +EOF + +for i in 0 1 7 8 9; do + F=$(eval echo \$F$i) + IN=$(eval echo \$IN$i) + OUT=$(eval echo \$OUT$i) + EXP=$(eval echo \$EXP$i) + REAL_REC=$(ltlsynt -f "$F" --input="$IN" --output="$OUT" \ + --realizability --algo=rec) + test $REAL_REC = UNREALIZABLE + REAL_QP=$(ltlsynt -f "$F" --input="$IN" --output="$OUT" \ + --realizability --algo=qp) + test $REAL_QP = UNREALIZABLE + SYNT=$(ltlsynt -f "$F" --input="$IN" --output="$OUT") + test $SYNT = UNREALIZABLE + PG=$(mktemp) +done + +for i in 2 3 4 5 6; do + F=$(eval echo \$F$i) + IN=$(eval echo \$IN$i) + OUT=$(eval echo \$OUT$i) + EXP=$(eval echo \$EXP$i) + REAL=$(ltlsynt -f "$F" --input="$IN" --output="$OUT" --realizability) + test $REAL = REALIZABLE + ltlsynt -f "$F" --input="$IN" --output="$OUT" > out$i + diff out$i exp$i +done