From b7cd47563259cda43d74926a7aa2b9f5eb770bac Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 6 May 2019 21:52:05 +0200 Subject: [PATCH] tl: first_match does not preserve syntactic_si * spot/tl/formula.cc: Fix it. * tests/core/kind.test: Add test case. --- spot/tl/formula.cc | 6 +++--- tests/core/kind.test | 2 ++ 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index ab01b15f5..f6f4dbcfa 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1632,10 +1632,10 @@ namespace spot break; case op::first_match: props = children[0]->props; - // If first_match(r) == r && !(r;[*]), then it should follow - // that if r is stutter-inv, then first_match(r) is - // stutter-inv, so we do not reset the syntactic_si bit. assert(is_.sere_formula); + // {(a[+];b*);c*}<>->d is stutter invariant + // {first_match(a[+];b*);c*}<>->d is NOT. + is_.syntactic_si = false; is_.boolean = false; is_.ltl_formula = false; is_.psl_formula = false; diff --git a/tests/core/kind.test b/tests/core/kind.test index e07fd02b9..db04fc6d2 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -136,6 +136,8 @@ Fa M b,&!xLPgopra (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla {b[+][:*0..3]},&!fPsopra {a->c[*]},xfPsopra +{(a[+];b*);c*}<>->d,&!xfPgopra +{first_match(a[+];b*);c*}<>->d,&!fPgopra EOF run 0 ../kind input