diff --git a/NEWS b/NEWS index 0c20a3125..474d2082e 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,7 @@ New in spot 1.99.5a (not yet released) - Nothing yet. + Bug fixes: + * automaton parser was ignoring the "unambiguous" property. New in spot 1.99.5 (2015-11-03) diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index 3f824db4a..fd5c3b0f5 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -436,6 +436,8 @@ header: format-version header-items res.h->aut->prop_stutter_sensitive(ss); bool iw = res.props.find("inherently-weak") != e; res.h->aut->prop_inherently_weak(iw); + bool iu = res.props.find("unambiguous") != e; + res.h->aut->prop_unambiguous(iu); } } diff --git a/src/tests/unambig.test b/src/tests/unambig.test index 24a826470..ed01baf58 100755 --- a/src/tests/unambig.test +++ b/src/tests/unambig.test @@ -170,5 +170,53 @@ State: 0 State: 1 State: 2 --END-- +HOA: v1 +AP: 0 +States: 3 +Start: 0 +Acceptance: 1 Inf(0) +properties: explicit-labels state-acc trans-labels unambiguous +--BODY-- +State: 0 +[t] 2 +[t] 1 +State: 1 +State: 2 +--END-- EOF -run 0 $autfilt -q --is-unambiguous input + +# Make sure we preserve the "unambiguous" property if it is given. +run 0 $autfilt -H --is-unambiguous input >output + +cat >expected <