Commit d9174593 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

common_trans: allow rewriting operators

Part of #168.

* spot/misc/formater.cc: Adjust to support bracketed options.
* bin/common_trans.hh, bin/common_trans.cc: Use that to
support rewriting operators.
* doc/org/ltlcross.org, tests/core/ltldo.test: Add some examples.
* NEWS: Mention it.
parent 925785e8
......@@ -20,6 +20,20 @@ New in spot 2.0a (not yet released)
These differ from --ap=RANGE that only consider *declared* atomic
propositions, regardless of whether they are actually used.
* ltlcross and ltldo have a new syntax to specify that an input
formula should be written in some given syntax after rewriting
some operators away. For instance the defaults arguments passed
to ltl2dstar have been changed from
--output-format=hoa %L %O
into
--output-format=hoa %[WM]L %O
where [WM] specifies that operators W and M should be rewritten
away. As a consequence running
ltldo ltl2dstar -f 'a M b'
will now work and call ltl2dstar on the equivalent formula
'b U (a & b)' instead. The operators that can be listed between
brackets are the same as those of ltlfilt --unabbreviate option.
Library:
* The print_hoa() function will now output version 1.1 of the HOA
......
......@@ -29,6 +29,7 @@
#include "error.h"
#include <spot/tl/print.hh>
#include <spot/tl/unabbrev.hh>
#include "common_conv.hh"
#include <spot/misc/escape.hh>
......@@ -41,11 +42,11 @@ static struct shorthands_t
shorthands[] = {
{ "lbt", " <%L>%O" },
{ "ltl2ba", " -f %s>%O" },
{ "ltl2dstar", " --output-format=hoa %L %O"},
{ "ltl2dstar", " --output-format=hoa %[MW]L %O"},
{ "ltl2tgba", " -H %f>%O" },
{ "ltl3ba", " -f %s>%O" },
{ "ltl3dra", " -f %s>%O" },
{ "modella", " %L %O" },
{ "modella", " %[MWei^]L %O" },
{ "spin", " -f %s>%O" },
};
......@@ -63,7 +64,7 @@ static void show_shorthands()
"matching those prefixes. So for instance\n"
" '{DRA} ~/mytools/ltl2dstar-0.5.2'\n"
"will changed into\n"
" '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %L %O'\n");
" '{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'\n");
}
......@@ -153,6 +154,58 @@ quoted_string::print(std::ostream& os, const char*) const
spot::quote_shell_string(os, val().c_str());
}
void quoted_formula::print(std::ostream& os, const char* pos) const
{
spot::formula f = val_;
if (*pos == '[')
{
++pos;
auto end = strchr(pos, ']');
auto arg = strndup(pos, end - pos);
f = spot::unabbreviate(f, arg);
free(arg);
pos = end + 1;
}
std::ostringstream ss;
std::ostream* out = &ss;
bool quoted = true;
switch (*pos)
{
case 'F':
case 'S':
case 'L':
case 'W':
out = &os;
quoted = false;
}
switch (*pos)
{
case 'f':
case 'F':
print_psl(*out, f, true);
break;
case 's':
case 'S':
print_spin_ltl(*out, f, true);
break;
case 'l':
case 'L':
print_lbt_ltl(*out, f);
break;
case 'w':
case 'W':
print_wring_ltl(*out, f);
break;
}
if (quoted)
{
std::string s = ss.str();
spot::quote_shell_string(os, s.c_str());
}
}
printable_result_filename::printable_result_filename()
{
val_ = nullptr;
......@@ -184,19 +237,42 @@ printable_result_filename::print(std::ostream& os, const char*) const
spot::quote_shell_string(os, val()->name());
}
void
filed_formula::print(std::ostream& os, const char* pos) const
{
std::ostringstream ss;
f_.print(ss, pos);
os << '\'' << string_to_tmp(ss.str(), serial_) << '\'';
}
std::string
filed_formula::string_to_tmp(const std::string str, unsigned n) const
{
char prefix[30];
snprintf(prefix, sizeof prefix, "lcr-i%u-", n);
spot::open_temporary_file* tmpfile = spot::create_open_tmpfile(prefix);
std::string tmpname = tmpfile->name();
int fd = tmpfile->fd();
ssize_t s = str.size();
if (write(fd, str.c_str(), s) != s
|| write(fd, "\n", 1) != 1)
error(2, errno, "failed to write into %s", tmpname.c_str());
tmpfile->close();
return tmpname;
}
translator_runner::translator_runner(spot::bdd_dict_ptr dict,
bool no_output_allowed)
: dict(dict)
{
declare('f', &string_ltl_spot);
declare('s', &string_ltl_spin);
declare('l', &string_ltl_lbt);
declare('w', &string_ltl_wring);
declare('F', &filename_ltl_spot);
declare('S', &filename_ltl_spin);
declare('L', &filename_ltl_lbt);
declare('W', &filename_ltl_wring);
declare('f', &ltl_formula);
declare('s', &ltl_formula);
declare('l', &ltl_formula);
declare('w', &ltl_formula);
declare('F', &filename_formula);
declare('S', &filename_formula);
declare('L', &filename_formula);
declare('W', &filename_formula);
declare('D', &output);
declare('H', &output);
declare('N', &output);
......@@ -229,61 +305,29 @@ translator_runner::translator_runner(spot::bdd_dict_ptr dict,
}
}
void
translator_runner::string_to_tmp(std::string& str, unsigned n,
std::string& tmpname)
{
char prefix[30];
snprintf(prefix, sizeof prefix, "lcr-i%u-", n);
spot::open_temporary_file* tmpfile = spot::create_open_tmpfile(prefix);
tmpname = tmpfile->name();
int fd = tmpfile->fd();
ssize_t s = str.size();
if (write(fd, str.c_str(), s) != s
|| write(fd, "\n", 1) != 1)
error(2, errno, "failed to write into %s", tmpname.c_str());
tmpfile->close();
}
const std::string&
std::string
translator_runner::formula() const
{
// Pick the most readable format we have...
if (!string_ltl_spot.val().empty())
return string_ltl_spot;
if (!string_ltl_spin.val().empty())
return string_ltl_spin;
if (!string_ltl_wring.val().empty())
return string_ltl_wring;
if (!string_ltl_lbt.val().empty())
return string_ltl_lbt;
if (has('f') || has('F'))
return spot::str_psl(ltl_formula, true);
if (has('s') || has('S'))
return spot::str_spin_ltl(ltl_formula, true);
if (has('l') || has('L'))
return spot::str_lbt_ltl(ltl_formula);
if (has('w') || has('W'))
return spot::str_wring_ltl(ltl_formula);
SPOT_UNREACHABLE();
return string_ltl_spot;
return spot::str_psl(ltl_formula, true);
}
void
translator_runner::round_formula(spot::formula f, unsigned serial)
{
if (has('f') || has('F'))
string_ltl_spot = spot::str_psl(f, true);
if (has('s') || has('S'))
string_ltl_spin = spot::str_spin_ltl(f, true);
if (has('l') || has('L'))
string_ltl_lbt = spot::str_lbt_ltl(f);
if (has('w') || has('W'))
string_ltl_wring = spot::str_wring_ltl(f);
if (has('F'))
string_to_tmp(string_ltl_spot, serial, filename_ltl_spot);
if (has('S'))
string_to_tmp(string_ltl_spin, serial, filename_ltl_spin);
if (has('L'))
string_to_tmp(string_ltl_lbt, serial, filename_ltl_lbt);
if (has('W'))
string_to_tmp(string_ltl_wring, serial, filename_ltl_wring);
ltl_formula = f;
filename_formula.new_round(serial);
}
volatile bool timed_out = false;
unsigned timeout_count = 0;
......@@ -407,6 +451,10 @@ static const argp_option options[] =
"If either %l, %L, or %T are used, any input formula that does "
"not use LBT-style atomic propositions (i.e. p0, p1, ...) will be "
"relabeled automatically.\n"
"The sequences %f,%s,%l,%w,%F,%S,%L,%W can optionally be \"infixed\""
" by a bracketed sequence of operators to unabbreviate before outputing"
" the formula. For instance %[MW]f will rewrite operators M and W"
" before outputing it.\n"
"Furthermore, if COMMANDFMT has the form \"{NAME}CMD\", then only CMD "
"will be passed to the shell, and NAME will be used to name the tool "
"in the output.", 4 },
......
......@@ -56,6 +56,31 @@ struct quoted_string final: public spot::printable_value<std::string>
void print(std::ostream& os, const char* pos) const override;
};
struct quoted_formula final: public spot::printable_value<spot::formula>
{
using spot::printable_value<spot::formula>::operator=;
void print(std::ostream& os, const char* pos) const override;
};
struct filed_formula final: public spot::printable
{
filed_formula(const quoted_formula& ltl) : f_(ltl)
{
}
void print(std::ostream& os, const char* pos) const override;
void new_round(unsigned serial)
{
serial_ = serial;
}
private:
const quoted_formula& f_;
unsigned serial_;
std::string string_to_tmp(const std::string str, unsigned n) const;
};
struct printable_result_filename final:
public spot::printable_value<spot::temporary_file*>
{
......@@ -75,14 +100,8 @@ class translator_runner: protected spot::formater
protected:
spot::bdd_dict_ptr dict;
// Round-specific variables
quoted_string string_ltl_spot;
quoted_string string_ltl_spin;
quoted_string string_ltl_lbt;
quoted_string string_ltl_wring;
quoted_string filename_ltl_spot;
quoted_string filename_ltl_spin;
quoted_string filename_ltl_lbt;
quoted_string filename_ltl_wring;
quoted_formula ltl_formula;
filed_formula filename_formula = ltl_formula;
// Run-specific variables
printable_result_filename output;
public:
......@@ -92,8 +111,7 @@ public:
// whether we accept the absence of output
// specifier
bool no_output_allowed = false);
void string_to_tmp(std::string& str, unsigned n, std::string& tmpname);
const std::string& formula() const;
std::string formula() const;
void round_formula(spot::formula f, unsigned serial);
};
......
......@@ -98,6 +98,14 @@ Performing sanity checks and gathering statistics...
No problem detected.
#+end_example
To handle tools that do not support some LTL operators, the character
sequences ~%f~, ~%s~, ~%l~, ~%w~, ~%F~, ~%S~, ~%L~, and ~%W~ can be
"infixed" by a bracketed list of operators to rewrite away. For
instance if a tool reads LTL formulas from a file in LBT's syntax, but
does not support operators ~M~ (strong until) and ~W~ (weak until),
use ~%[WM]L~ instead of just ~%L~; this way operators ~W~ and ~M~ will
be rewritten using the other supported operators.
=ltlcross= can only read four kinds of output:
- Never claims (only if they are restricted to representing an
automaton using =if=, =goto=, and =skip= statements) such as those
......@@ -125,7 +133,7 @@ tools:
- '=ltl2ba -f %s >%O='
- '=ltl3ba -M0 -f %s >%O=' (less deterministic output, can be smaller)
- '=ltl3ba -M1 -f %s >%O=' (more deterministic output)
- '=modella -r12 -g -e %L %O='
- '=modella -r12 -g -e %[MWei^]L %O='
- '=/path/to/script4lbtt.py %L %O=' (script supplied by [[http://web.archive.org/web/20070214050826/http://estragon.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for
its interface with LBTT)
- '=ltl2tgba -s %f >%O=' (smaller output, Büchi automaton)
......@@ -134,22 +142,22 @@ tools:
- '=ltl2tgba -H -D %f >%O=' (more deterministic output, TGBA)
- '=lbt <%L >%O='
- '~ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD
--output-format=hoa %L %O~' deterministic Rabin output in HOA, as
--output-format=hoa %[MW]L %O~' deterministic Rabin output in HOA, as
supported since version 0.5.2 of =ltl2dstar=.
- '~ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD --automata=streett
--output-format=hoa %L %O~' deterministic Streett output in HOA,
--output-format=hoa %[MW]L %O~' deterministic Streett output in HOA,
as supported since version 0.5.2 of =ltl2dstar=.
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L %O=' (Rabin
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %[MW]L %O=' (Rabin
output in DSTAR format, as supported in older versions of
=ltl2dstar=.
- '=ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-sD %L - | dstar2tgba
-s >%O=' (external conversion from Rabin to Büchi done by
=dstar2tgba= for more reduction of the Büchi automaton than what
=ltlcross= would provide)
- '=java -jar Rabinizer.jar -ltl2dstar %F %O; mv %O.dst %O=' (Rabinizer
- '=java -jar Rabinizer.jar -ltl2dstar %[MW]F %O; mv %O.dst %O=' (Rabinizer
uses the last =%O= argument as a prefix to which it always append =.dst=,
so we have to rename =%O.dst= as =%O= so that =ltlcross= can find the file)
- '~java -jar rabinizer3.1.jar -in=formula -silent -out=std -format=hoa -auto=tr %f >%O~'
- '~java -jar rabinizer3.1.jar -in=formula -silent -out=std -format=hoa -auto=tr %[MWR]f >%O~'
(rabinizer 3.1 can output automata in the HOA format)
- '=ltl3dra -f %s >%O=' (The HOA format is the default for =ltl2dra=.)
......@@ -167,18 +175,18 @@ the following words, then the string on the right is appended.
lbt <%L>%O
ltl2ba -f %s>%O
ltl2dstar --output-format=hoa %L %O
ltl2dstar --output-format=hoa %[MW]L %O
ltl2tgba -H %f>%O
ltl3ba -f %s>%O
ltl3dra -f %f>%O
modella %L %O
ltl3dra -f %s>%O
modella %[MWei^]L %O
spin -f %s>%O
Any {name} and directory component is skipped for the purpose of
matching those prefixes. So for instance
'{DRA} ~/mytools/ltl2dstar-0.5.2'
will changed into
'{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %L %O'
'{DRA} ~/mytools/ltl2dstar-0.5.2 --output-format=hoa %[MR]L %O'
#+end_example
What this implies is that running =ltlcross ltl2ba ltl3ba ...= is
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2016 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -20,9 +20,18 @@
#include "config.h"
#include <spot/misc/formater.hh>
#include <iostream>
#include <sstream>
namespace spot
{
static void unclosed_bracket(const char* s)
{
std::ostringstream ss;
ss << '\'' << s << "' has unclosed bracket";
throw std::runtime_error(ss.str());
}
void
formater::scan(const char* fmt, std::vector<bool>& has) const
{
......@@ -30,6 +39,19 @@ namespace spot
if (*pos == '%')
{
char c = *++pos;
// %[...]c
const char* mark = pos;
if (c == '[')
{
do
{
++pos;
if (SPOT_UNLIKELY(!*pos))
unclosed_bracket(mark - 1);
}
while (*pos != ']');
c = *++pos;
}
has[c] = true;
if (!c)
break;
......@@ -53,9 +75,25 @@ namespace spot
else
{
char c = *++pos;
const char* next = pos;
// in case we have %[...]X... , we want to pass
// [...]X... to the printer, and continue after the X once
// that is done.
if (c == '[')
{
do
{
++next;
if (SPOT_UNLIKELY(*next == 0))
unclosed_bracket(pos - 1);
}
while (*next != ']');
c = *++next;
}
call_[c]->print(*output_, pos);
if (!c)
break;
pos = next;
}
return *output_;
}
......
......@@ -25,10 +25,11 @@ ltldo=ltldo
ltl2tgba=ltl2tgba
genltl=genltl
run 0 $ltldo -f a -f 'a&b' -t 'echo %f,%s' >output
run 0 $ltldo -f a -f 'a&b' -f 'a -> b' -t 'echo %f,%s,%[ei]w' >output
cat >expected <<EOF
a,a
(a) & (b),(a) && (b)
a,a,a=1
(a) & (b),(a) && (b),(a=1) * (b=1)
(a) -> (b),(a) -> (b),(a=0) + (b=1)
EOF
diff output expected
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment