Commit 171ca678 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Introduce EConcatMarked "<>+>" as operator.

* src/ltlast/binop.cc, src/ltlast/binop.hh: Introduce
EConcatMarked ("<>+>").
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/simpfg.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.cc: Deal with it if possible or ignore
it.
parent 66317db4
......@@ -123,6 +123,8 @@ namespace spot
return "M";
case EConcat:
return "EConcat";
case EConcatMarked:
return "EConcatMarked";
case UConcat:
return "UConcat";
}
......@@ -256,6 +258,7 @@ namespace spot
}
break;
case EConcat:
case EConcatMarked:
// - 0 <>-> Exp = 0
// - 1 <>-> Exp = Exp
// - #e <>-> Exp = 0
......
......@@ -55,6 +55,7 @@ namespace spot
W, //< weak until
M, //< strong release (dual of weak until)
EConcat, // Existential Concatenation
EConcatMarked, // Existential Concatenation, Marked
UConcat // Universal Concatenation
};
......
......@@ -263,6 +263,7 @@ namespace spot
case binop::Implies:
case binop::EConcat:
case binop::UConcat:
case binop::EConcatMarked:
result_ = binop::instance(bo->op(),
basic_reduce(f1),
basic_reduce(f2));
......
......@@ -64,6 +64,7 @@ namespace spot
case binop::R:
case binop::EConcat:
case binop::UConcat:
case binop::EConcatMarked:
assert(!"unsupported operator");
break;
}
......
......@@ -89,6 +89,7 @@ namespace spot
case binop::M:
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
result_ = binop::instance(op, f1, f2);
return;
}
......
......@@ -186,6 +186,13 @@ namespace spot
binop::UConcat : binop::EConcat,
recurse_(f1, false), recurse(f2));
return;
case binop::EConcatMarked:
/* !(a <>-> b) == a[]-> !b */
result_ = binop::instance(negated_ ?
binop::UConcat :
binop::EConcatMarked,
recurse_(f1, false), recurse(f2));
return;
}
/* Unreachable code. */
assert(0);
......
......@@ -158,6 +158,7 @@ namespace spot
return;
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
return;
}
/* Unreachable code. */
......@@ -318,7 +319,8 @@ namespace spot
case binop::Implies:
case binop::UConcat:
case binop::EConcat:
break;
case binop::EConcatMarked:
return;
case binop::U:
/* a < b => a U b = b */
......
......@@ -53,6 +53,7 @@ namespace spot
case binop::Equiv:
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
result_ = binop::instance(op, f1, f2);
return;
/* true U f2 == F(f2) */
......
......@@ -128,6 +128,7 @@ namespace spot
case binop::Implies:
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
return;
case binop::U:
case binop::W:
......@@ -363,6 +364,7 @@ namespace spot
case binop::Implies:
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
return;
case binop::U:
/* (a < c) && (c < d) => a U b < c U d */
......
......@@ -110,6 +110,7 @@ namespace spot
{
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
os_ << "{ ";
top_level_ = true;
bo->first()->accept(*this);
......@@ -150,6 +151,9 @@ namespace spot
case binop::EConcat:
os_ << " }<>-> ";
break;
case binop::EConcatMarked:
os_ << " }<>+> ";
break;
}
bo->second()->accept(*this);
......@@ -342,6 +346,11 @@ namespace spot
os_ << " <>-> ";
bo->second()->accept(*this);
break;
case binop::EConcatMarked:
bo->first()->accept(*this);
os_ << " <>+> ";
bo->second()->accept(*this);
break;
/* W and M are not supported by Spin */
case binop::W:
bo->first()->accept(*this);
......@@ -350,7 +359,7 @@ namespace spot
break;
case binop::M:
bo->first()->accept(*this);
os_ << " M ";
os_ << " M ";
bo->second()->accept(*this);
break;
}
......
......@@ -114,6 +114,7 @@ namespace spot
case binop::M:
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
assert(!"unsupported operator");
}
/* Unreachable code. */
......
......@@ -131,6 +131,7 @@ namespace spot
case binop::M:
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
assert(!"unsupported operator");
}
/* Unreachable code. */
......
......@@ -249,6 +249,7 @@ namespace spot
assert(0); // TBD
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
assert(!"unsupported operator");
}
/* Unreachable code. */
......
......@@ -222,6 +222,7 @@ namespace spot
}
case binop::UConcat:
case binop::EConcat:
case binop::EConcatMarked:
assert(!"unsupported operator");
break;
}
......
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