diff --git a/NEWS b/NEWS index 58ba086e6..1119bdbc5 100644 --- a/NEWS +++ b/NEWS @@ -1,30 +1,45 @@ New in spot 1.1.4a (not relased) + * Changes to command-line tools: + + - ltlcross has a new option --color to color its output. It is + enabled by default when the output is a terminal. + + - ltlcross will give an example of infinite word accepted by the + two automata when the product between a positive automaton and a + negative automaton is non-empty. + + - ltlcross can now read the Rabin and Streett automata output by + ltl2dstar. This type of output should be specified using '%D': + + ltlcross 'ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-s %L %D' + + However because Spot only supports Büchi acceptance, these Rabin + and Streett automata are immediately converted to TGBA before + further processing by ltlcross. This is still interesting to + search for bugs in translators to Rabin or Streett automata, but + the statistics might not be very relevant. + + - To help with debugging problems detected by ltlcross, the + environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where + temporary files are created and if they should be erased. Read + the man page of ltlcross for details. + + - There is a new command, named dstar2tgba, that converts a + deterministic Rabin or Streett automaton as output by + ltl2dstar into a TGBA, BA or Monitor. When a deterministic + Rabin automaton is realizable by a deterministic Büchi automaton, + the conversion preserve determinism. (This is not implemented + for Streett.) + + - The %S escape sequence used by ltl2tgba --stats to display the + number of SCCs in the output automaton has been renamed to %c. + This makes it more homogeneous with the --stats option of the + new dstar2tgba command. + * All the parsers implemented in Spot now use the same type to store locations. - * ltlcross has a new option --color to color its output. It is enabled - by default when the output is a terminal. - - * ltlcross will give an example of infinite word accepted by the - two automata when the product between a positive automaton and - a negative automaton is non-empty. - - * ltlcross can now read the Rabin and Streett automata output by - ltl2dstar. This type of output should be specified using '%D': - - ltlcross 'ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-s %L %D' - - However because Spot only supports Büchi acceptance, these Rabin - and Streett automata are immediately converted to TGBA before - further processing by ltlcross. This is still interesting to - search for bugs in translators to Rabin or Streett automata, but - the statistics might not be very relevant. - - * Environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where - temporary files are created and if they should be erased. Read - the man page of ltlcross for detail. - * Degeneralization was not indempotant on automata with an accepting initial state that was on a cycle, but without self-loop. diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 4782aa4ee..904c7e9b1 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -546,12 +546,12 @@ ltl2tgba --help | sed -n '/^ *%/p' #+RESULTS: : %% a single % : %a number of acceptance sets +: %c number of SCCs : %d 1 if the automaton is deterministic, 0 otherwise : %e number of edges : %f the formula, in Spot's syntax : %n number of nondeterministic states : %s number of states -: %S number of SCCs : %t number of transitions For instance we can study the size of the automata generated for the diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 560c32434..97972dcf0 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -42,7 +42,8 @@ libcommon_a_SOURCES = \ common_setup.hh \ common_sys.hh -bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross +bin_PROGRAMS = ltlfilt genltl randltl ltl2tgba ltl2tgta ltlcross \ + dstar2tgba # Dummy program used just to generate man/spot-x.7 in a way that is # consistent with the other man pages (e.g., with a version number that @@ -55,5 +56,6 @@ randltl_SOURCES = randltl.cc ltl2tgba_SOURCES = ltl2tgba.cc ltl2tgta_SOURCES = ltl2tgta.cc ltlcross_SOURCES = ltlcross.cc +dstar2tgba_SOURCES = dstar2tgba.cc spot_x_SOURCES = spot-x.cc ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME) diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc new file mode 100644 index 000000000..683b4c749 --- /dev/null +++ b/src/bin/dstar2tgba.cc @@ -0,0 +1,372 @@ +// -*- 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 . + +#include "common_sys.hh" + +#include +#include + +#include +#include "error.h" + +#include "common_setup.hh" +#include "common_finput.hh" +#include "common_cout.hh" +#include "common_post.hh" + +#include "ltlast/formula.hh" +#include "tgba/tgbaexplicit.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/lbtt.hh" +#include "tgbaalgos/neverclaim.hh" +#include "tgbaalgos/save.hh" +#include "tgbaalgos/stats.hh" +#include "tgba/bddprint.hh" +#include "misc/optionmap.hh" +#include "dstarparse/public.hh" +#include "tgbaalgos/scc.hh" + +const char argp_program_doc[] ="\ +Convert Rabin and Streett automata into Büchi automata.\n\n\ +This reads the output format of ltl2dstar and will output a \n\ +Transition-based Generalized Büchi Automata in GraphViz's format by default.\n\ +If multiple files are supplied (one automaton per file), several automata\n\ +will be output."; + +#define OPT_TGBA 1 +#define OPT_DOT 2 +#define OPT_LBTT 3 +#define OPT_SPOT 4 +#define OPT_STATS 5 + +static const argp_option options[] = + { + /**************************************************/ + { 0, 0, 0, 0, "Input:", 1 }, + { "file", 'F', "FILENAME", 0, + "process the automaton in FILENAME", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Output automaton type:", 2 }, + { "tgba", OPT_TGBA, 0, 0, + "Transition-based Generalized Büchi Automaton (default)", 0 }, + { "ba", 'B', 0, 0, "Büchi Automaton", 0 }, + { "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes " + "of the given formula)", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Output format:", 3 }, + { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, + "LBTT's format (add =t to force transition-based acceptance even" + " on Büchi automata)", 0 }, + { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 }, + { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 }, + { "utf8", '8', 0, 0, "enable UTF-8 characters in output " + "(ignored with --lbtt or --spin)", 0 }, + { "stats", OPT_STATS, "FORMAT", 0, + "output statistics about the automaton", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\ + "the following interpreted sequences (capitals for input," + " minuscules for output):", 4 }, + { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "name of the input file", 0 }, + { "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of states", 0 }, + { "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of edges", 0 }, + { "%T, %t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of transitions", 0 }, + { "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of acceptance pairs or sets", 0 }, + { "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of SCCs", 0 }, + { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "number of nondeterministic states in output", 0 }, + { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "1 if the output is deterministic, 0 otherwise", 0 }, + { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "a single %", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { "extra-options", 'x', "OPTS", 0, + "fine-tuning options (see spot-x (7))", 0 }, + { 0, 0, 0, 0, 0, 0 } + }; + +const struct argp_child children[] = + { + { &post_argp, 0, 0, 20 }, + { &misc_argp, 0, 0, -1 }, + { 0, 0, 0, 0 } + }; + +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot; +bool utf8 = false; +const char* stats = ""; +spot::option_map extra_options; + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case '8': + spot::enable_utf8(); + break; + case 'B': + type = spot::postprocessor::BA; + break; + case 'F': + jobs.push_back(job(arg, true)); + break; + case 'M': + type = spot::postprocessor::Monitor; + break; + case 's': + format = Spin; + if (type != spot::postprocessor::Monitor) + type = spot::postprocessor::BA; + break; + case 'x': + { + const char* opt = extra_options.parse_options(arg); + if (opt) + error(2, 0, "failed to parse --options near '%s'", opt); + } + break; + case OPT_DOT: + format = Dot; + break; + case OPT_LBTT: + if (arg) + { + if (arg[0] == 't' && arg[1] == 0) + format = Lbtt_t; + else + error(2, 0, "unknown argument for --lbtt: '%s'", arg); + } + else + { + format = Lbtt; + } + break; + case OPT_SPOT: + format = Spot; + break; + case OPT_STATS: + if (!*arg) + error(2, 0, "empty format string for --stats"); + stats = arg; + format = Stats; + break; + case OPT_TGBA: + if (format == Spin) + error(2, 0, "--spin and --tgba are incompatible"); + type = spot::postprocessor::TGBA; + break; + case ARGP_KEY_ARG: + jobs.push_back(job(arg, true)); + break; + + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + + +namespace +{ + /// \brief prints various statistics about a TGBA + /// + /// This object can be configured to display various statistics + /// about a TGBA. Some %-sequence of characters are interpreted in + /// the format string, and replaced by the corresponding statistics. + class dstar_stat_printer: protected spot::stat_printer + { + public: + dstar_stat_printer(std::ostream& os, const char* format) + : spot::stat_printer(os, format) + { + declare('A', &daut_acc_); + declare('C', &daut_scc_); + declare('E', &daut_edges_); + declare('F', &filename_); + declare('f', &filename_); // Override the formula printer. + declare('S', &daut_states_); + declare('T', &daut_trans_); + } + + /// \brief print the configured statistics. + /// + /// The \a f argument is not needed if the Formula does not need + /// to be output. + std::ostream& + print(const spot::dstar_aut* daut, const spot::tgba* aut, + const char* filename) + { + filename_ = filename; + + if (has('T')) + { + spot::tgba_sub_statistics s = sub_stats_reachable(daut->aut); + daut_states_ = s.states; + daut_edges_ = s.transitions; + daut_trans_ = s.sub_transitions; + } + else if (has('E')) + { + spot::tgba_sub_statistics s = sub_stats_reachable(daut->aut); + daut_states_ = s.states; + daut_edges_ = s.transitions; + } + else if (has('S')) + { + daut_states_ = daut->aut->num_states(); + } + + if (has('A')) + daut_acc_ = daut->accpair_count; + + if (has('C')) + { + spot::scc_map m(daut->aut); + m.build_map(); + daut_scc_ = m.scc_count(); + } + + return this->spot::stat_printer::print(aut); + } + + private: + spot::printable_value filename_; + spot::printable_value daut_states_; + spot::printable_value daut_edges_; + spot::printable_value daut_trans_; + spot::printable_value daut_acc_; + spot::printable_value daut_scc_; + }; + + + class dstar_processor: public job_processor + { + public: + spot::postprocessor& post; + dstar_stat_printer statistics; + + dstar_processor(spot::postprocessor& post) + : post(post), statistics(std::cout, stats) + { + } + + int + process_formula(const spot::ltl::formula*, const char*, int) + { + assert(!"should not happen"); + return 0; + } + + + int + process_file(const char* filename) + { + spot::dstar_parse_error_list pel; + spot::dstar_aut* daut; + spot::bdd_dict dict; + daut = spot::dstar_parse(filename, pel, &dict); + if (spot::format_dstar_parse_errors(std::cerr, filename, pel)) + { + delete daut; + return 2; + } + if (!daut) + { + error(2, 0, "failed to read automaton from %s", filename); + } + spot::tgba* nba = spot::dstar_to_tgba(daut); + const spot::tgba* aut = post.run(nba, 0); + + if (utf8) + { + spot::tgba* a = const_cast(aut); + if (spot::tgba_explicit_formula* tef = + dynamic_cast(a)) + tef->enable_utf8(); + else if (spot::sba_explicit_formula* sef = + dynamic_cast(a)) + sef->enable_utf8(); + } + + switch (format) + { + case Dot: + spot::dotty_reachable(std::cout, aut, + (type == spot::postprocessor::BA) + || (type == spot::postprocessor::Monitor)); + break; + case Lbtt: + spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); + break; + case Lbtt_t: + spot::lbtt_reachable(std::cout, aut, false); + break; + case Spot: + spot::tgba_save_reachable(std::cout, aut); + break; + case Spin: + spot::never_claim_reachable(std::cout, aut); + break; + case Stats: + // FIXME: filename + statistics.print(daut, aut, filename) << "\n"; + break; + } + delete aut; + delete daut; + flush_cout(); + return 0; + } + }; +} + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { options, parse_opt, "[FILENAMES...]", + argp_program_doc, children, 0, 0 }; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) + exit(err); + + if (jobs.empty()) + jobs.push_back(job("-", true)); + + spot::postprocessor post(&extra_options); + post.set_pref(pref); + post.set_type(type); + post.set_level(level); + + dstar_processor processor(post); + if (processor.run()) + return 2; + return 0; +} diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 70cb71bf0..d137d455f 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -86,7 +86,7 @@ static const argp_option options[] = { "%t", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of transitions", 0 }, { "%a", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, - { "%S", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 }, + { "%c", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of SCCs", 0 }, { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "number of nondeterministic states", 0 }, { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE, diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index cdaec3555..4ad43e7cd 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -23,6 +23,7 @@ convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \ "$(PERL)" "$(top_srcdir)/tools/help2man -N -L 'en_US.UTF-8'" dist_man1_MANS = \ + dstar2tgba.1 \ genltl.1 \ ltl2tgba.1 \ ltl2tgta.1 \ @@ -35,6 +36,9 @@ dist_man7_MANS = \ MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS) EXTRA_DIST = $(dist_man1_MANS:.1=.x) $(dist_man7_MANS:.7=.x) +dstar2tgba.1: $(common_dep) $(srcdir)/dstar2tgba.x $(srcdir)/../dstar2tgba.cc + $(convman) ../dstar2tgba$(EXEEXT) $(srcdir)/dstar2tgba.x $@ + ltl2tgba.1: $(common_dep) $(srcdir)/ltl2tgba.x $(srcdir)/../ltl2tgba.cc $(convman) ../ltl2tgba$(EXEEXT) $(srcdir)/ltl2tgba.x $@ diff --git a/src/bin/man/dstar2tgba.x b/src/bin/man/dstar2tgba.x new file mode 100644 index 000000000..ce7cec939 --- /dev/null +++ b/src/bin/man/dstar2tgba.x @@ -0,0 +1,32 @@ +[NAME] +dstar2tgba \- convert Rabin or Streett automata into Büchi automata +[BIBLIOGRAPHY] +.TP +1. + + +Documents the output format of ltl2dstar. + +.TP +2. +Chistof Löding: Mehods for the Transformation of ω-Automata: +Complexity and Connection to Second Order Logic. Diploma Thesis. +University of Kiel. 1998. + +Describes various tranformations from non-deterministic Rabin and +Streett automata to Büchi automata. Slightly optimized variants of +these transformations are used by dstar2tgba for the general cases. + +.TP +3. +Sriram C. Krishnan, Anuj Puri, and Robert K. Brayton: Deterministic +ω-automata vis-a-vis Deterministic Büchi Automata. ISAAC'94. + +Explains how to preserve the determinism of Rabin and Streett automata +when the property can be repreted by a Deterministic automaton. +dstar2tgba implements this for the Rabin case only. In other words, +translating a deterministic Rabin automaton with dstar2tgba will +produce a deterministic TGBA or BA if such a automaton exists. + +[SEE ALSO] +.BR spot-x (7) diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index 55d1e56a5..cd7d99534 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2011, 2012 Laboratoire de Recherche et Développement +// Copyright (C) 2008, 2011, 2012, 2013 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -142,12 +142,13 @@ namespace spot : format_(format) { declare('a', &acc_); + declare('c', &scc_); declare('d', &deterministic_); declare('e', &edges_); declare('f', &form_); declare('n', &nondetstates_); declare('s', &states_); - declare('S', &scc_); + declare('S', &scc_); // Historical. Deprecated. Use %c instead. declare('t', &trans_); set_output(os); prime(format); @@ -176,7 +177,7 @@ namespace spot if (has('a')) acc_ = aut->number_of_acceptance_conditions(); - if (has('S')) + if (has('c') || has('S')) { scc_map m(aut); m.build_map(); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 3bbd2614c..bf88f1052 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -111,6 +111,7 @@ TESTS = \ wdba2.test \ babiak.test \ ltl2dstar.test \ + ltl2dstar2.test \ randtgba.test \ emptchk.test \ emptchke.test \ diff --git a/src/tgbatest/ltl2dstar.test b/src/tgbatest/ltl2dstar.test index decdca4cb..1419dd8d2 100755 --- a/src/tgbatest/ltl2dstar.test +++ b/src/tgbatest/ltl2dstar.test @@ -33,6 +33,7 @@ ltl2tgba=../../bin/ltl2tgba ltlcross=../../bin/ltlcross randltl=../../bin/randltl ltlfilt=../../bin/ltlfilt +dstar2tgba=../../bin/dstar2tgba $ltlfilt -f 'a U b' -l | ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - - | @@ -62,11 +63,16 @@ EOF diff expected out +RAB=--automata=rabin +STR=--automata=streett + $randltl -n 15 a b | $ltlfilt --nnf --remove-wm | $ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \ ---timeout=10 \ +--timeout=30 \ "$ltl2tgba -s %f >%N" \ -"ltl2dstar --automata=rabin --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \ -"ltl2dstar --automata=rabin --ltl2nba=spin:$ltl2tgba@-s %L %D" \ -"ltl2dstar --automata=streett --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \ -"ltl2dstar --automata=streett --ltl2nba=spin:$ltl2tgba@-s %L %D" +"ltl2dstar $RAB --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \ +"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \ +"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \ +"ltl2dstar $STR --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \ +"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" \ +"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" diff --git a/src/tgbatest/ltl2dstar2.test b/src/tgbatest/ltl2dstar2.test new file mode 100755 index 000000000..452655f04 --- /dev/null +++ b/src/tgbatest/ltl2dstar2.test @@ -0,0 +1,77 @@ +#!/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 . + +# Do some quick translations to make sure the neverclaims produced by +# spot actually look correct! We do that by parsing them via ltlcross. +# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed. + +. ./defs +set -e + +# Skip this test if ltl2dstar is not installed. +(ltl2dstar --version) || exit 77 + +ltlfilt=../../bin/ltlfilt +ltl2tgba=../../bin/ltl2tgba +dstar2tgba=../../bin/dstar2tgba +randltl=../../bin/randltl + + +# Make sure all recurrence formulas are translated into deterministic +# Büchi automata by the DRA->TGBA converster. + +$randltl -n -1 a b --tree-size=5..15 | +$ltlfilt --syntactic-recurrence --remove-wm -r -u \ + --size-min=4 --size-max=15 --relabel=abc | +head -n 20 > formulas + +$randltl -n -1 a b --tree-size=5..15 | +$ltlfilt -v --obligation | +$ltlfilt --syntactic-recurrence --remove-wm -r -u \ + --size-min=4 --size-max=15 --relabel=abc | +head -n 20 >> formulas + +while read f; do + $ltlfilt -f "$f" -l | + ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - foo + echo "$f" + det=`$dstar2tgba foo --stats '%d'` + test $det -eq 1; +done < formulas + + +# Now make sure that some obviously non-deterministic property +# are not translated to deterministic. + +cat >formulas <GFb +GFa & FGb +FGa | FGb +FGa & FGb +EOF + +while read f; do + $ltlfilt -f "$f" -l | + ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - foo + echo "$f" + det=`$dstar2tgba foo --stats '%d'` + test $det -eq 0; +done < formulas