From 0c7c9338054f0353935168e4f5e2752676ae039f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 12 May 2013 17:49:20 +0200 Subject: [PATCH] simulation: Fix co-simulation and iterated simulations of BA automata * src/tgbaalgos/simulation.hh, src/tgbaalgos/simulation.cc (simulation_sba, cosimulation_sba, iterated_simulations_sba): New function. Also speedup the existing functions by avoiding add_acceptince_conditions() and add_conditions(). Finally, use scc_filter_states() when dealing with degeneralized automata. * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh (do_ba_simul): New method. Use it after degeneralization. * src/tgba/tgbaexplicit.hh (get_transition, get_state): New methods. * src/tgbatest/basimul.test: New file. * src/tgbatest/Makefile.am (TESTS): Add it. * NEWS: Introduce the new function and summarize the bug. --- NEWS | 17 +++ src/tgba/tgbaexplicit.hh | 27 +++- src/tgbaalgos/postproc.cc | 19 ++- src/tgbaalgos/postproc.hh | 1 + src/tgbaalgos/simulation.cc | 258 ++++++++++++++++++++++-------------- src/tgbaalgos/simulation.hh | 12 +- src/tgbatest/Makefile.am | 1 + src/tgbatest/basimul.test | 76 +++++++++++ 8 files changed, 302 insertions(+), 109 deletions(-) create mode 100755 src/tgbatest/basimul.test diff --git a/NEWS b/NEWS index 1c92839bd..0d6ef5072 100644 --- a/NEWS +++ b/NEWS @@ -30,6 +30,15 @@ New in spot 1.1a (not yet released): the automaton. scc_filter_state() should be used when post-processing TGBAs that actually represent BAs. + - simulation_sba(), cosimulation_sba(), and + iterated_simulations_sba() are new functions that apply to TGBAs + that actually represent BAs. They preserve the imporant + property that if a state of the BA is is accepting, the outgoing + transitions of that state are all accepting in the TGBA that + represent the BA. This is something that was not preserved by + functions cosimultion() and iterated_simulations() as mentionned + in the bug fixes below. + - ltlcross has a new option --seed, that makes it possible to change the seed used by the random graph generator. @@ -40,6 +49,14 @@ New in spot 1.1a (not yet released): - ltlfilt --stutter-invariant would trigger an assert on PSL formulas. - ltl2tgba, ltl2tgta, ltlcross, and ltlfilt, would all choke on empty lines in a file of formulas. They now ignore empty lines. + - The iterated simulation applied on degeneralized TGBA was bogus + for two reasons: one was that cosimulation was applied using the + generic cosimulation for TGBA, and the second is that + SCC-filtering, performed between iterations, was also a + TGBA-based algorithm. Both of these algorithms could lose the + property that if a TGBA represents a BA, all the outgoing + transitions of a state should be accepting. As a consequence, some + formulas where translated to incorrect Büchi automata. New in spot 1.1 (2013-04-28): diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index 6b6f35f61..375891d7a 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche +// et Développement de l'Epita. // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -318,6 +318,15 @@ namespace spot return const_cast(&(*(si->get_iterator()))); } + transition* + get_transition(const tgba_succ_iterator* si) + { + const tgba_explicit_succ_iterator* tmp + = down_cast*>(si); + assert(tmp); + return get_transition(tmp); + } + void add_condition(transition* t, const ltl::formula* f) { t->condition &= formula_to_bdd(f, dict_, this); @@ -336,12 +345,24 @@ namespace spot return dict_->is_registered_acceptance_variable(f, this); } - //old tgba explicit labelled interface + //old tgba explicit labeled interface bool has_state(const label_t& name) { return ls_.find(name) != ls_.end(); } + /// \brief Return the state associated to a given label. + /// + /// This is similar to add_state(), except that it returns 0 if + /// the state does not exist. + const State* get_state(const label_t& name) + { + typename ls_map::const_iterator i = ls_.find(name); + if (i == ls_.end()) + return 0; + return &i->second; + } + const label_t& get_label(const State* s) const { typename sl_map::const_iterator i = sl_.find(s); diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 0d636c915..df70a2abe 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -80,6 +80,23 @@ namespace spot } } + const tgba* postprocessor::do_ba_simul(const tgba* a, int opt) + { + switch (opt) + { + case 0: + return a; + case 1: + return simulation_sba(a); + case 2: + return cosimulation_sba(a); + case 3: + default: + return iterated_simulations_sba(a); + } + } + + const tgba* postprocessor::do_degen(const tgba* a) { const tgba* d = degeneralize(a, @@ -90,7 +107,7 @@ namespace spot if (ba_simul_ <= 0) return d; - const tgba* s = do_simul(d, ba_simul_); + const tgba* s = do_ba_simul(d, ba_simul_); if (s != d) delete d; diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index c5575fc6c..a3bbd3c40 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -91,6 +91,7 @@ namespace spot protected: const tgba* do_simul(const tgba* input, int opt); + const tgba* do_ba_simul(const tgba* input, int opt); const tgba* do_degen(const tgba* input); output_type type_; diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 3f82aad65..1ee61ed89 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -212,7 +212,6 @@ namespace spot return false; } - int transitions; int states; }; @@ -223,7 +222,7 @@ namespace spot // automaton is similar to the old one, except that the acceptance // condition on the transitions are complemented. // There is a specialization below. - template + template class acc_compl_automaton: public tgba_reachable_iterator_depth_first { @@ -243,16 +242,10 @@ namespace spot const state*, int, const tgba_succ_iterator* si) { - bdd acc = ReverseComplement - ? ac_.reverse_complement(si->current_acceptance_conditions()) - : ac_.complement(si->current_acceptance_conditions()); - - const tgba_explicit_succ_iterator* tmpit = - down_cast*>(si); + bdd acc = ac_.complement(si->current_acceptance_conditions()); typename tgba_explicit_number::transition* t = - ea_->get_transition(tmpit); + ea_->get_transition(si); t->acceptance_conditions = acc; } @@ -281,10 +274,10 @@ namespace spot acc_compl ac_; }; - // The specialization for Cosimulation equals to true: We need to - // copy. - template <> - class acc_compl_automaton: + // The specialization for Cosimulation equals to true: We copy the + // automaton and transpose it at the same time. + template + class acc_compl_automaton: public tgba_reachable_iterator_depth_first { public: @@ -292,13 +285,16 @@ namespace spot : tgba_reachable_iterator_depth_first(a), size(0), out_(new tgba_explicit_number(a->get_dict())), - ea_(a), - ac_(ea_->all_acceptance_conditions(), - ea_->neg_acceptance_conditions()), + ac_(a->all_acceptance_conditions(), + a->neg_acceptance_conditions()), current_max(0) { - init_ = ea_->get_init_state(); + a->get_dict()->register_all_variables_of(a, out_); + out_->set_acceptance_conditions(a->all_acceptance_conditions()); + + const state* init_ = a->get_init_state(); out_->set_init_state(get_state(init_)); + init_->destroy(); } inline unsigned @@ -325,19 +321,32 @@ namespace spot unsigned src = get_state(in_s); unsigned dst = get_state(out_s); - // In the case of the cosimulation, we want to have all the - // ingoing transition, and to keep the rest of the code - // similar, we just create equivalent transition in the other - // direction. Since we do not have to run through the - // automaton to get the signature, this is correct. - std::swap(src, dst); - - bdd acc = ac_.complement(si->current_acceptance_conditions()); + // Note the order of src and dst: the transition is reversed. tgba_explicit_number::transition* t - = out_->create_transition(src, dst); + = out_->create_transition(dst, src); - out_->add_acceptance_conditions(t, acc); - out_->add_conditions(t, si->current_condition()); + t->condition = si->current_condition(); + if (!Sba) + { + bdd acc = ac_.complement(si->current_acceptance_conditions()); + t->acceptance_conditions = acc; + } + else + { + // If the acceptance is interpreted as state-based, to + // apply the reverse simulation on a SBA, we should pull + // the acceptance of the destination state on its incoming + // arcs (which now become outgoing args after + // transposition). + tgba_succ_iterator* it = out_->succ_iter(out_s); + it->first(); + if (!it->done()) + { + bdd acc = ac_.complement(it->current_acceptance_conditions()); + t->acceptance_conditions = acc; + } + delete it; + } } void process_state(const state*, int, tgba_succ_iterator*) @@ -347,8 +356,6 @@ namespace spot ~acc_compl_automaton() { - // Because we don't know what get_init_state returns... - init_->destroy(); } public: @@ -359,16 +366,14 @@ namespace spot map_state_state old_name_; private: - const state* init_; - const tgba* ea_; acc_compl ac_; map_state_unsigned state2int; unsigned current_max; }; // The direct_simulation. If Cosimulation is true, we are doing a - // cosimulation. Seems obvious, but it's better to be clear. - template + // cosimulation. + template class direct_simulation { protected: @@ -393,7 +398,7 @@ namespace spot scc_map_->build_map(); old_a_ = a_; - acc_compl_automaton acc_compl(a_); + acc_compl_automaton acc_compl(a_); // We'll start our work by replacing all the acceptance // conditions by their complement. @@ -401,7 +406,7 @@ namespace spot // Contains the relation between the names of the states in // the automaton returned by the complementation and the one - // get in argument to the constructor of acc_compl. + // passed to the constructor of acc_compl. std::swap(old_name_, acc_compl.old_name_); a_ = acc_compl.out_; @@ -417,9 +422,10 @@ namespace spot // class. We register one bdd by state, because in the worst // case, |Class| == |State|. unsigned set_num = a_->get_dict() - ->register_anonymous_variables(size_a_ + 1, a_); + ->register_anonymous_variables(size_a_ + 1, this); - all_proms_ = bdd_support(a_->all_acceptance_conditions()); + all_acceptance_conditions_ = a_->all_acceptance_conditions(); + all_proms_ = bdd_support(all_acceptance_conditions_); bdd_initial = bdd_ithvar(set_num++); bdd init = bdd_ithvar(set_num++); @@ -451,7 +457,6 @@ namespace spot relation_[init] = init; std::swap(order_, acc_compl.order_); - all_acceptance_conditions_ = a_->all_acceptance_conditions(); } @@ -460,16 +465,17 @@ namespace spot // function simulation. virtual ~direct_simulation() { + a_->get_dict()->unregister_all_my_variables(this); delete scc_map_; + if (!dont_delete_old_) - delete old_a_; - // Since a_ is a new automaton only if we are doing a - // cosimulation. + delete old_a_; + // a_ is a new automaton only if we are doing a cosimulation. if (Cosimulation) delete a_; } - // We update the name of the classes. + // Update the name of the classes. void update_previous_class() { std::list::iterator it_bdd = used_var_.begin(); @@ -535,35 +541,37 @@ namespace spot { const state* dst = sit->current_state(); bdd acc = bddtrue; - map_constraint::const_iterator it; - // We are using new_original_[old_name_[...]] because we - // give the constraints in the original automaton, so we - // need to use this heavy computation. - if (map_cst_ - && ((it = map_cst_ - ->find(std::make_pair(new_original_[old_name_[src]], - new_original_[old_name_[dst]]))) - != map_cst_->end())) - { - acc = it->second; - } - else - { - acc = sit->current_acceptance_conditions(); - } - // to_add is a conjunction of the acceptance condition, - // the label of the transition and the class of the - // destination and all the class it implies. - bdd to_add = acc & sit->current_condition() - & relation_[previous_class_[dst]]; + map_constraint::const_iterator it; + // We are using new_original_[old_name_[...]] because + // we have the constraints in the original automaton + // which has been duplicated twice to get the current + // automaton. + if (map_cst_ + && ((it = map_cst_ + ->find(std::make_pair(new_original_[old_name_[src]], + new_original_[old_name_[dst]]))) + != map_cst_->end())) + { + acc = it->second; + } + else + { + acc = sit->current_acceptance_conditions(); + } + + // to_add is a conjunction of the acceptance condition, + // the label of the transition and the class of the + // destination and all the class it implies. + bdd to_add = acc & sit->current_condition() + & relation_[previous_class_[dst]]; - res |= to_add; - dst->destroy(); - } + res |= to_add; + dst->destroy(); + } // When we Cosimulate, we add a special flag to differentiate - // initial state. + // the initial state from the other. if (Cosimulation && initial_state == src) res |= bdd_initial; @@ -728,10 +736,10 @@ namespace spot acc_compl reverser(all_acceptance_conditions_, a_->neg_acceptance_conditions()); - tgba_explicit_number* res - = new tgba_explicit_number(a_->get_dict()); - res->set_acceptance_conditions - (all_acceptance_conditions_); + bdd_dict* d = a_->get_dict(); + tgba_explicit_number* res = new tgba_explicit_number(d); + d->register_all_variables_of(a_, res); + res->set_acceptance_conditions(all_acceptance_conditions_); bdd sup_all_acc = bdd_support(all_acceptance_conditions_); // Non atomic propositions variables (= acc and class) @@ -746,11 +754,16 @@ namespace spot // The difference between the two next lines is: // the first says "if you see A", the second "if you - // see A and all the class implied by it". + // see A and all the classes implied by it". bdd2state[part] = current_max; bdd2state[relation_[part]] = current_max; } + // Acceptance of states. Only used if Sba && Cosimulation. + std::vector accst; + if (Sba && Cosimulation) + accst.resize(current_max + 1, bddfalse); + stat.states = bdd_lstate_.size(); stat.transitions = 0; @@ -788,7 +801,7 @@ namespace spot bddtrue); all_atomic_prop -= one; - // For each possible valuation, iterator over all possible + // For each possible valuation, iterate over all possible // destination classes. We use minato_isop here, because // if the same valuation of atomic properties can go // to two different classes C1 and C2, iterating on @@ -815,13 +828,13 @@ namespace spot // Keep only ones who are acceptance condition. bdd acc = bdd_existcomp(cond_acc_dest, sup_all_acc); - // Keep the other ! + // Keep the other! bdd cond = bdd_existcomp(cond_acc_dest, sup_all_atomic_prop); // Because we have complemented all the acceptance - // condition on the input automaton, we must re - // invert them to create a new transition. + // conditions on the input automaton, we must + // revert them to create a new transition. acc = reverser.reverse_complement(acc); // Take the id of the source and destination. To @@ -842,9 +855,12 @@ namespace spot // Create the transition, add the condition and the // acceptance condition. tgba_explicit_number::transition* t - = res->create_transition(src , dst); - res->add_conditions(t, cond); - res->add_acceptance_conditions(t, acc); + = res->create_transition(src, dst); + t->condition = cond; + if (Sba && Cosimulation) + accst[dst] = acc; + else + t->acceptance_conditions = acc; } } } @@ -854,6 +870,23 @@ namespace spot res->merge_transitions(); + // Mark all accepting state in a second pass, when + // dealing with SBA in cosimulation. + if (Sba && Cosimulation) + for (unsigned snum = current_max; snum > 0; --snum) + { + const state* s = res->get_state(snum); + tgba_succ_iterator* it = res->succ_iter(s); + bdd acc = accst[snum]; + for (it->first(); !it->done(); it->next()) + { + tgba_explicit_number::transition* t = + res->get_transition(it); + t->acceptance_conditions = acc; + } + delete it; + } + res_is_deterministic = nb_minato == nb_satoneset; return res; @@ -968,7 +1001,7 @@ namespace spot }; // For now, we don't try to handle cosimulation. - class direct_simulation_dont_care: public direct_simulation + class direct_simulation_dont_care: public direct_simulation { typedef std::vector > constraints; typedef std::map(t) + : direct_simulation(t) { // This variable is used in the new signature. on_cycle_ = - bdd_ithvar(a_->get_dict()->register_anonymous_variables(1, a_)); + bdd_ithvar(a_->get_dict()->register_anonymous_variables(1, this)); // This one is used for the iteration on all the // possibilities. Avoid computing two times "no constraints". @@ -1000,7 +1033,6 @@ namespace spot & all_class_var_ & on_cycle_); } - // This function computes the don't care signature of the state // src. This signature is similar to the classic one, excepts // that if the transition is on a SCC, we add a on_cycle_ on it, @@ -1481,7 +1513,7 @@ namespace spot else if (cstr.empty()) empty_seen_ = true; - direct_simulation dir_sim(original_, &cstr); + direct_simulation dir_sim(original_, &cstr); tgba* tmp = dir_sim.run(); automaton_size cur_size = dir_sim.get_stat(); if (*min == 0 || min_size_ > cur_size) @@ -1529,21 +1561,35 @@ namespace spot tgba* simulation(const tgba* t) { - direct_simulation simul(t); + direct_simulation simul(t); + return simul.run(); + } + tgba* + simulation_sba(const tgba* t) + { + direct_simulation simul(t); return simul.run(); } tgba* cosimulation(const tgba* t) { - direct_simulation simul(t); + direct_simulation simul(t); + return simul.run(); + } + tgba* + cosimulation_sba(const tgba* t) + { + direct_simulation simul(t); return simul.run(); } + + template tgba* - iterated_simulations(const tgba* t) + iterated_simulations_(const tgba* t) { tgba* res = const_cast (t); automaton_size prev; @@ -1552,8 +1598,7 @@ namespace spot do { prev = next; - direct_simulation simul(res); - + direct_simulation simul(res); tgba* maybe_res = simul.run(); if (res != t) @@ -1566,24 +1611,34 @@ namespace spot } unique_ptr after_simulation(maybe_res); - - direct_simulation cosimul(after_simulation); - + direct_simulation cosimul(after_simulation); unique_ptr after_cosimulation(cosimul.run()); - next = cosimul.get_stat(); - - res = scc_filter(after_cosimulation, false); + if (Sba) + res = scc_filter_states(after_cosimulation); + else + res = scc_filter(after_cosimulation, false); } while (prev != next); - return res; } + tgba* + iterated_simulations(const tgba* t) + { + return iterated_simulations_(t); + } + + tgba* + iterated_simulations_sba(const tgba* t) + { + return iterated_simulations_(t); + } + tgba* dont_care_simulation(const tgba* t, int limit) { - direct_simulation sim(t); + direct_simulation sim(t); tgba* tmp = sim.run(); direct_simulation_dont_care s(tmp); @@ -1613,12 +1668,9 @@ namespace spot if (res != t) delete res; - direct_simulation cosimul(after_simulation); - + direct_simulation cosimul(after_simulation); unique_ptr after_cosimulation(cosimul.run()); - next = cosimul.get_stat(); - res = scc_filter(after_cosimulation, true); } while (prev != next); diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index 5f9ca29c3..d85d9935c 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,7 +20,6 @@ #ifndef SPOT_TGBAALGOS_SIMULATION_HH # define SPOT_TGBAALGOS_SIMULATION_HH - namespace spot { class tgba; @@ -28,6 +27,7 @@ namespace spot /// \addtogroup tgba_reduction /// @{ + /// @{ /// \brief Attempt to reduce the automaton by direct simulation. /// /// When the suffixes (letter and acceptance conditions) reachable @@ -68,7 +68,10 @@ namespace spot /// \return a new automaton which is at worst a copy of the received /// one tgba* simulation(const tgba* automaton); + tgba* simulation_sba(const tgba* automaton); + /// @} + /// @{ /// \brief Attempt to reduce the automaton by reverse simulation. /// /// When the prefixes (letter and acceptance conditions) leading to @@ -116,7 +119,10 @@ namespace spot /// \return a new automaton which is at worst a copy of the received /// one tgba* cosimulation(const tgba* automaton); + tgba* cosimulation_sba(const tgba* automaton); + /// @} + /// @{ /// \brief Iterate simulation() and cosimulation(). /// /// Runs simulation(), cosimulation(), and scc_filter() in a loop, @@ -132,6 +138,8 @@ namespace spot /// \return a new automaton which is at worst a copy of the received /// one tgba* iterated_simulations(const tgba* automaton); + tgba* iterated_simulations_sba(const tgba* automaton); + /// @} tgba* dont_care_simulation(const tgba* t, int limit = -1); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index a080ce6ec..00cc920a3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -110,6 +110,7 @@ TESTS = \ dfs.test \ emptchkr.test \ ltlcounter.test \ + basimul.test \ spotlbtt.test \ ltlcross.test \ spotlbtt2.test \ diff --git a/src/tgbatest/basimul.test b/src/tgbatest/basimul.test new file mode 100755 index 000000000..30cb71bf2 --- /dev/null +++ b/src/tgbatest/basimul.test @@ -0,0 +1,76 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2013 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 + +set -e + +ltl2tgba=../../bin/ltl2tgba + + +# This bug was found while working on the state-based acceptance +# output for the LBTT format. Using ba-simul=2 causes reverse +# simulation to be applied to the BA automaton obtained after +# degeneralization. Unfortunately in Spot 1.1, reverse simulation is +# only implemented on TGBA, and when applied to a TGBA that is a BA, +# it may merge one state that is accepting with one state that is not +# accepting, just because they have the same incoming transitions. +# (Applying direct simulation on a TGBA that is a BA is not a problem, +# since an accepting state will never have the same outgoing +# transitions as a BA.) + +# In previous tests, we did not notice the bug because the --lbtt +# output was always using transition-based acceptance (the equivalent +# of --lbtt=t today), so the result of the reverse-simulation on the +# BA was output as a TGBA with a single acceptance set, and some state +# had both accepting and non-accepting transitions because of the +# merge. Unfortunately, this is not a Büchi automaton. Using the +# --spin output, or the new (state-based) --lbtt output highlights the +# bug. + +# In the cases below, the following configurations used to fail +# cross-comparison with the other "sane" configurations, at least +# with the first formula. (The other three formulas were added because +# they also triggered related issues while debugging the first one.) +# --lbtt -x ba-simul=2 +# --lbtt -x ba-simul=3 +# --spin -x ba-simul=2 +# --spin -x ba-simul=3 + + +for seed in 1 2 3; do + ../../bin/ltlcross --seed=$seed --density=0.$seed \ + -f 'X((F(Xa | b) W c) U (Xc W (a & d)))' \ + -f '((<> p5 V ((p0 U p1) <-> (p5 \/ p1))) -> ((<> p4 V p2) M p2))' \ + -f '!p2 & (Fp5 R (((p0 U p1) & (p5 | p1)) | (!p5 & (!p0 R !p1))))' \ + -f '! ((p0 /\ p4) <-> ! ((! p0 U (p0 W p4)) /\ (X p5 -> ([] p3 /\ p5))))' \ + "$ltl2tgba --ba --high --lbtt=t -x ba-simul=0 %f >%T" \ + "$ltl2tgba --ba --high --lbtt=t -x ba-simul=1 %f >%T" \ + "$ltl2tgba --ba --high --lbtt=t -x ba-simul=2 %f >%T" \ + "$ltl2tgba --ba --high --lbtt=t -x ba-simul=3 %f >%T" \ + "$ltl2tgba --ba --high --lbtt -x ba-simul=0 %f >%T" \ + "$ltl2tgba --ba --high --lbtt -x ba-simul=1 %f >%T" \ + "$ltl2tgba --ba --high --lbtt -x ba-simul=2 %f >%T" \ + "$ltl2tgba --ba --high --lbtt -x ba-simul=3 %f >%T" \ + "$ltl2tgba --ba --high --spin -x ba-simul=0 %f >%N" \ + "$ltl2tgba --ba --high --spin -x ba-simul=1 %f >%N" \ + "$ltl2tgba --ba --high --spin -x ba-simul=2 %f >%N" \ + "$ltl2tgba --ba --high --spin -x ba-simul=3 %f >%N" +done -- GitLab