diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 770fd920e..a6eeddae0 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -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 diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index de97074c9..d2653ef5b 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -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 }; diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index d94dedfc5..35474254d 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -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)); diff --git a/src/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc index cd9fb416c..44fa95b0f 100644 --- a/src/ltlvisit/consterm.cc +++ b/src/ltlvisit/consterm.cc @@ -64,6 +64,7 @@ namespace spot case binop::R: case binop::EConcat: case binop::UConcat: + case binop::EConcatMarked: assert(!"unsupported operator"); break; } diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 76ddbf01d..30ccf50da 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -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; } diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 1f573dfd9..8ce7f66a3 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -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); diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 8bae2b143..1c5974611 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -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 */ diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index e6da46304..b6567e282 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -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) */ diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 3888e287b..0034834e8 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -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 */ diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index ec968f82a..d47493926 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -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; } diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 6db6b8ece..8bae93f3d 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -114,6 +114,7 @@ namespace spot case binop::M: case binop::UConcat: case binop::EConcat: + case binop::EConcatMarked: assert(!"unsupported operator"); } /* Unreachable code. */ diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 03842d756..34731c90d 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -131,6 +131,7 @@ namespace spot case binop::M: case binop::UConcat: case binop::EConcat: + case binop::EConcatMarked: assert(!"unsupported operator"); } /* Unreachable code. */ diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index c57ad9927..81c22ca54 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -249,6 +249,7 @@ namespace spot assert(0); // TBD case binop::UConcat: case binop::EConcat: + case binop::EConcatMarked: assert(!"unsupported operator"); } /* Unreachable code. */ diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index 2fa3eedc8..85503e88f 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -222,6 +222,7 @@ namespace spot } case binop::UConcat: case binop::EConcat: + case binop::EConcatMarked: assert(!"unsupported operator"); break; }