Commit 59202bd5 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

do not rewrite <-> and -> for Spin LTL output

Fixes #39, reported by Joachim Klein.

* src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Take an option
to specify which of xor/equiv/implies should be rewritten.
* src/ltlvisit/print.cc (print_spin): Rewrite only xor.
* src/tests/ltlfilt.test: Add a test case.
* NEWS: Mention this.
parent ac6b042e
......@@ -26,6 +26,8 @@ New in spot 1.99.2a (not yet released)
double quotes where not always properly rendered.
- A spurious assertion was triggered by streett_to_generalized_buchi(),
but only when compiled in DEBUG mode.
- LTL formula rewritten in Spin's syntax no longer have their ->
and <-> rewritten aways.
New in spot 1.99.2 (2015-07-18)
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -29,8 +29,25 @@ namespace spot
namespace ltl
{
unabbreviate_logic_visitor::unabbreviate_logic_visitor()
unabbreviate_logic_visitor::unabbreviate_logic_visitor(const char* opt)
{
while (*opt)
switch (char c = *opt++)
{
case '^':
rewrite_xor = true;
break;
case 'i':
rewrite_i = true;
break;
case 'e':
rewrite_e = true;
break;
default:
throw std::runtime_error
(std::string("unknown option for unabbreviate_logic_visitor(): ")
+ c);
}
}
unabbreviate_logic_visitor::~unabbreviate_logic_visitor()
......@@ -42,29 +59,44 @@ namespace spot
{
const formula* f1 = recurse(bo->first());
const formula* f2 = recurse(bo->second());
binop::type op = bo->op();
switch (op)
{
/* f1 ^ f2 == !(f1 <-> f2) */
/* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */
case binop::Xor:
{
const formula* a =
multop::instance(multop::And, f1->clone(),
unop::instance(unop::Not, f2->clone()));
const formula* b =
multop::instance(multop::And, f2,
unop::instance(unop::Not, f1));
result_ = multop::instance(multop::Or, a, b);
return;
if (!rewrite_xor)
goto no_rewrite;
if (!rewrite_e)
{
result_ = unop::instance(unop::Not,
binop::instance(binop::Equiv, f1, f2));
return;
}
else
{
const formula* a =
multop::instance(multop::And, f1->clone(),
unop::instance(unop::Not, f2->clone()));
const formula* b =
multop::instance(multop::And, f2,
unop::instance(unop::Not, f1));
result_ = multop::instance(multop::Or, a, b);
return;
}
}
/* f1 => f2 == !f1 | f2 */
case binop::Implies:
if (!rewrite_i)
goto no_rewrite;
result_ = multop::instance(multop::Or,
unop::instance(unop::Not, f1), f2);
return;
/* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */
case binop::Equiv:
if (!rewrite_e)
goto no_rewrite;
{
const formula* f1c = f1->clone();
const formula* f2c = f2->clone();
......@@ -90,6 +122,7 @@ namespace spot
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
no_rewrite:
result_ = binop::instance(op, f1, f2);
return;
}
......@@ -99,15 +132,16 @@ namespace spot
const formula*
unabbreviate_logic_visitor::recurse(const formula* f)
{
return unabbreviate_logic(f);
f->accept(*this);
return result_;
}
const formula*
unabbreviate_logic(const formula* f)
unabbreviate_logic(const formula* f, const char* xie)
{
if (f->is_sugar_free_boolean())
return f->clone();
unabbreviate_logic_visitor v;
unabbreviate_logic_visitor v(xie);
f->accept(v);
return v.result();
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -44,13 +44,17 @@ namespace spot
{
typedef clone_visitor super;
public:
unabbreviate_logic_visitor();
unabbreviate_logic_visitor(const char* opt = "^ie");
virtual ~unabbreviate_logic_visitor();
using super::visit;
void visit(const binop* bo);
virtual const formula* recurse(const formula* f);
private:
bool rewrite_xor = false;
bool rewrite_i = false;
bool rewrite_e = false;
};
/// \ingroup ltl_rewriting
......@@ -60,7 +64,12 @@ namespace spot
/// This will rewrite binary operators such as binop::Implies,
/// binop::Equals, and binop::Xor, using only unop::Not, multop::Or,
/// and multop::And.
SPOT_API const formula* unabbreviate_logic(const formula* f);
///
/// The optional \a opt argument can be a string containing any
/// subset of the string "^ie" to denote the operators (xor,
/// implication, equivalence) to actually remove.
SPOT_API const formula* unabbreviate_logic(const formula* f,
const char* opt = "^ie");
}
}
......@@ -121,8 +121,8 @@ namespace spot
"true", // 1 doesn't work from the command line
"[*0]", // not supported
" xor ", // rewritten
" -> ", // rewritten, although supported
" <-> ", // rewritten, although supported
" -> ",
" <-> ",
" U ",
" V ",
" W ", // rewritten
......@@ -985,8 +985,8 @@ namespace spot
std::ostream&
print_spin_ltl(std::ostream& os, const formula* f, bool full_parent)
{
// Remove xor, ->, and <-> first.
const formula* fu = unabbreviate_logic(f);
// Rewrite xor.
const formula* fu = unabbreviate_logic(f, "^");
// Also remove W and M.
f = unabbreviate_wm(fu);
fu->destroy();
......
......@@ -50,7 +50,6 @@ G(a & Xb)
Xa
F(a & !Xa & Xb)
{a & {b|c} }
EOF
checkopt --eventual <<EOF
......@@ -161,6 +160,7 @@ b & GF(a | c) & FG(a | c)
G(d & e) | FG(Xf| !c) | h | i
b & !Xc & e & (f | g)
b & GF(a | c) & !GF!(a | c)
F(a <-> b) -> (c xor d)
EOF
cat >exp <<EOF
......@@ -168,6 +168,7 @@ p0 & Xp1
p0 & p1 & GF(p0 | p2) & FG(p0 | p2)
p0 & GFp1 & FGp1
p0 | Gp1 | FG(p2 | Xp3)
p0 | Gp1
EOF
run 0 $ltlfilt -u --nnf --relabel-bool=pnn in >out
......@@ -189,11 +190,55 @@ p0 && []<>p1 && <>[]p1
#define p2 (!c)
#define p3 (f)
p0 || []p1 || <>[](p2 || Xp3)
#define p0 ((c && !d) || (!c && d))
#define p1 ((a && !b) || (!a && b))
p0 || []p1
EOF
run 0 $ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
diff exp out
cat >exp <<EOF
#define p0 (a)
#define p1 (c)
#define p2 (b)
p0 && p1 && Xp2
#define p0 (a)
#define p1 (b)
#define p2 (c)
p0 && p1 && []<>(p0 || p2) && <>[](p0 || p2)
#define p0 (b)
#define p1 (a)
#define p2 (c)
p0 && []<>(p1 || p2) && <>[](p1 || p2)
#define p0 (h)
#define p1 (i)
#define p2 (d)
#define p3 (e)
#define p4 (c)
#define p5 (f)
p0 || p1 || [](p2 && p3) || <>[](!p4 || Xp5)
#define p0 (b)
#define p1 (e)
#define p2 (f)
#define p3 (g)
#define p4 (c)
p0 && p1 && (p2 || p3) && !Xp4
#define p0 (b)
#define p1 (a)
#define p2 (c)
p0 && []<>(p1 || p2) && ![]<>!(p1 || p2)
#define p0 (a)
#define p1 (b)
#define p2 (c)
#define p3 (d)
<>(p0 <-> p1) -> !(p2 <-> p3)
EOF
run 0 $ltlfilt -s -u --relabel=pnn --define in >out
diff exp out
toolong='((p2=0) * (p3=1))' # work around the 80-col check
cat >exp <<EOF
#define p0 ((a=1))
#define p1 ((c=1))
......@@ -220,6 +265,11 @@ cat >exp <<EOF
#define p3 ((g=1))
#define p4 ((c=1))
(p0=1) * (p1=1) * ((p2=1) + (p3=1)) * (X(p4=0))
#define p0 ((c=1))
#define p1 ((d=1))
#define p2 ((a=1))
#define p3 ((b=1))
((p0=1) * (p1=0)) + ((p0=0) * (p1=1)) + (G(((p2=1) * (p3=0)) + $toolong))
EOF
run 0 $ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
diff exp out
......@@ -233,6 +283,7 @@ b & GF(a | c) & FG(a | c)@
h | i | G(d & e) | FG(!c | Xf)@
b & e & (f | g) & !Xc@
b & GF(a | c) & !GF!(a | c)@
F(a <-> b) -> (c xor d)@
EOF
diff exp out
......
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