From 6a2aad62595654f10da780f47b6739ad72c6ea64 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 9 Jan 2015 22:25:18 +0100 Subject: [PATCH] never: add an option to output in Spin's 6.2.4 style Fixes #46. * src/tgbaalgos/neverclaim.cc: Add option '6'. * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Make it possible to use the option. * NEWS, doc/org/oaut.org: Document it. * src/tgbatest/ltlcross2.test: Test it. --- NEWS | 17 +++++++---- doc/org/oaut.org | 25 +++++++++++++++- src/bin/common_aoutput.cc | 9 ++++-- src/bin/dstar2tgba.cc | 9 ++++-- src/tgbaalgos/neverclaim.cc | 59 ++++++++++++++++++++++++++++++------- src/tgbatest/ltlcross2.test | 5 ++-- 6 files changed, 101 insertions(+), 23 deletions(-) diff --git a/NEWS b/NEWS index 299c43dd7..6121f32d7 100644 --- a/NEWS +++ b/NEWS @@ -65,17 +65,24 @@ New in spot 1.99a (not yet released) - LTL formulas can include /* comments */. + - GraphViz output now uses an horizontal layout by default. + The --dot option of the various command-line tools takes an + optional parameter to fine-tune the GraphViz output (including + vertical layout, round states, and named automata). + + - Never claims can now be output in the style usd by Spin since + version 6.2.4 (i.e., using do..od instead of if..fi, and with + atomic statements for terminal acceptance). The default output + is still the old one for compatibility with existing tools. The + new style can be requested from command-line tools using option + --spin=6 (or -s6 for short). + - Spot is now compiling in C++11 mode. The set of features we use requires GCC >= 4.6 or Clang >= 3.1. These minimum versions are old enough that it should not be an issue to most people. - Boost is not used anymore. - - GraphViz output now uses an horizontal layout by default. - The --dot option of the various command-line tools takes an - optional parameter to fine-tune the GraphViz output (including - vertical layout, round states, and named automata). - - The tgba_succ_iterator interface has changed. Methods next(), and first() should now return a bool indicating whether the current iteration is valid. diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 6b5462b37..123f0f2bc 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -416,7 +416,7 @@ ltl2tgba -s 'a U b' #+END_SRC #+RESULTS: -: never { +: never { /* a U b */ : T0_init: : if : :: ((b)) -> goto accept_all @@ -426,6 +426,29 @@ ltl2tgba -s 'a U b' : skip : } +Recent versions of Spin (starting with Spin 6.2.4) output never claims +in a slightly different style that can be requested using either +=-s6= or =--spin=6=: + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -s6 'a U b' +#+END_SRC + +#+RESULTS: +: never { /* a U b */ +: T0_init: +: do +: :: atomic { ((b)) -> assert(!((b))) } +: :: ((a) && (!(b))) -> goto T0_init +: od; +: accept_all: +: skip +: } + +(Note that while Spot is able to read never claims that follow any of +these two styles, it is not capable of interpreting an arbitrary piece +of Promela syntax.) + * Dot output The =--dot= option (which usually is the default) causes automata to be diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 833732c79..c64e7cb60 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -34,6 +34,7 @@ automaton_format_t automaton_format = Dot; static const char* opt_dot = nullptr; +static const char* opt_never = nullptr; static const char* hoa_opt = nullptr; const char* opt_name = nullptr; static const char* stats = ""; @@ -63,7 +64,9 @@ static const argp_option options[] = { "name", OPT_NAME, "FORMAT", 0, "set the name of the output automaton", 0 }, { "quiet", 'q', 0, 0, "suppress all normal output", 0 }, - { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 }, + { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)." + " Add letters to select (6) Spin's 6.2.4 style, (c) comments on states", + 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 }, @@ -161,6 +164,8 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) automaton_format = Spin; if (type != spot::postprocessor::Monitor) type = spot::postprocessor::BA; + if (arg) + opt_never = arg; break; case OPT_DOT: automaton_format = Dot; @@ -249,7 +254,7 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut, spot::tgba_save_reachable(std::cout, aut); break; case Spin: - spot::never_claim_reachable(std::cout, aut); + spot::never_claim_reachable(std::cout, aut, opt_never); break; case Stats: statistics.print(haut, aut, f, filename, loc, time) << '\n'; diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index cc23132d1..d22d7efde 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -85,7 +85,9 @@ static const argp_option options[] = " on Büchi automata)", 0 }, { "name", OPT_NAME, "FORMAT", 0, "set the name of the output automaton", 0 }, - { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 }, + { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)." + " Add letters to select (6) Spin's 6.2.4 style, (c) comments on states", + 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 }, @@ -137,6 +139,7 @@ static output_format format = Dot; static const char* opt_dot = nullptr; static const char* stats = ""; static const char* hoa_opt = nullptr; +static const char* opt_never = nullptr; static const char* opt_name = nullptr; static spot::option_map extra_options; @@ -166,6 +169,8 @@ parse_opt(int key, char* arg, struct argp_state*) format = Spin; if (type != spot::postprocessor::Monitor) type = spot::postprocessor::BA; + if (arg) + opt_never = arg; break; case 'x': { @@ -366,7 +371,7 @@ namespace spot::tgba_save_reachable(std::cout, aut); break; case Spin: - spot::never_claim_reachable(std::cout, aut); + spot::never_claim_reachable(std::cout, aut, opt_never); break; case Stats: statistics.print(daut, aut, filename, conversion_time) << '\n'; diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 13a82d269..7624317d3 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -38,9 +38,11 @@ namespace spot public: std::ostream& os_; bool opt_comments_ = false; + bool opt_624_ = false; const_tgba_digraph_ptr aut_; bool fi_needed_ = false; bool need_accept_all_ = false; + unsigned accept_all_ = 0; public: never_claim_output(std::ostream& os, const char* options) @@ -50,6 +52,9 @@ namespace spot while (char c = *options++) switch (c) { + case '6': + opt_624_ = true; + break; case 'c': opt_comments_ = true; break; @@ -73,7 +78,11 @@ namespace spot end() const { if (need_accept_all_) - os_ << "accept_all:\n skip\n"; + { + os_ << "accept_all:"; + print_comment(accept_all_); + os_ << "\n skip\n"; + } os_ << '}' << std::endl; } @@ -85,6 +94,13 @@ namespace spot return (it->cond == bddtrue) && (it->dst == n) && (++it == ts.end()); } + void + print_comment(unsigned n) const + { + if (opt_comments_) + os_ << " /* " << aut_->format_state(n) << " */"; + } + void print_state(unsigned n) const { @@ -114,33 +130,54 @@ namespace spot { // We want the accept_all state at the end of the never claim. need_accept_all_ = true; + accept_all_ = n; return; } print_state(n); os_ << ':'; - if (opt_comments_) - os_ << " /* " << aut_->format_state(n) << " */"; - os_ << "\n if\n"; + print_comment(n); + os_ << (opt_624_ ? "\n do\n" : "\n if\n"); bool did_output = false; - for (auto&t : aut_->out(n)) + for (auto& t: aut_->out(n)) { did_output = true; - os_ << " :: ("; + bool atom = + opt_624_ && aut_->state_is_accepting(t.dst) && is_sink(t.dst); + if (atom) + os_ << " :: atomic { ("; + else + os_ << " :: ("; const ltl::formula* f = bdd_to_formula(t.cond, aut_->get_dict()); to_spin_string(f, os_, true); + if (atom) + { + os_ << ") -> assert(!("; + to_spin_string(f, os_, true); + os_ << ")) }"; + } + else + { + os_ << ") -> goto "; + print_state(t.dst); + } f->destroy(); - os_ << ") -> goto "; - print_state(t.dst); os_ << '\n'; } if (!did_output) { - os_ << " :: (false) -> goto "; - print_state(n); + if (opt_624_) + { + os_ << " :: atomic { (false) -> assert(!(false)) }"; + } + else + { + os_ << " :: (false) -> goto "; + print_state(n); + } os_ << '\n'; } - os_ << " fi;\n"; + os_ << (opt_624_ ? " od;\n" : " fi;\n"); } void print(const const_tgba_digraph_ptr& aut) diff --git a/src/tgbatest/ltlcross2.test b/src/tgbatest/ltlcross2.test index 6d34a9983..acc5b3e48 100755 --- a/src/tgbatest/ltlcross2.test +++ b/src/tgbatest/ltlcross2.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -40,6 +40,7 @@ ltl2tgba=../../bin/ltl2tgba "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \ "$ltl2tgba --spin --ba -x degen-skip=0 %f >%N" \ "$ltl2tgba --lbtt --ba --high %f > %T" \ +"$ltl2tgba --spin=6 --ba --medium %f > %N" \ "$ltl2tgba --hoa -BDC %f > %H" \ "$ltl2tgba --lbtt -BC %f > %T" \ --json=output.json --csv=output.csv