diff --git a/ChangeLog b/ChangeLog index 97d9b9f49..44856bfe9 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-01-27 Alexandre Duret-Lutz + + Report formulas that are both safety and guarantee. + + * src/tgbatest/ltl2tgba.cc (-O): Report formulas that are both + safety and guarantee. + * src/tgbatest/obligation.test: Add cases. + 2011-01-27 Alexandre Duret-Lutz Rename is_safety_automaton() as is_guarantee_automaton() and diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 50a127da9..adf950cb0 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1152,16 +1152,23 @@ main(int argc, char** argv) } else { - if (is_guarantee_automaton(minimized)) + bool g = is_guarantee_automaton(minimized); + bool s = is_safety_mwdba(minimized); + if (g && !s) { std::cout << "this is a guarantee property (hence, " << "an obligation property)"; } - else if (is_safety_mwdba(minimized)) + else if (s && !g) { std::cout << "this is a safety property (hence, " << "an obligation property)"; } + else if (s && g) + { + std::cout << "this is a guarantee and a safety property" + << " (and of course an obligation property)"; + } else { std::cout << "this is an obligation property that is " diff --git a/src/tgbatest/obligation.test b/src/tgbatest/obligation.test index 882385a4d..970df7305 100755 --- a/src/tgbatest/obligation.test +++ b/src/tgbatest/obligation.test @@ -80,6 +80,9 @@ NO G(q->(p->(!r U (s&!r&X(!r U t))))U(r|G(p->(s&XFt)))) NO G(p->F(s&!z&X(!z U t))) NO G(q->G(p->(s&!z&X(!z U t)))) NO G(q->(p->(!r U (s&!r&!z&X((!r&!z) U t))))U(r|G(p->(s&!z&X(!z U t))))) +GS p +GS q&Xp +GS G(Ga&F!a) EOF grok() @@ -87,6 +90,7 @@ grok() case $1 in "this is a safety property"*) echo SA;; "this is a guarantee property"*) echo GU;; + "this is a guarantee and a safety"*) echo GS;; "this is an obligation property"*) echo OB;; "this is not an obligation property"*) echo NO;; *) echo XX;; @@ -107,6 +111,7 @@ while read exp f; do case $resx,$resy in SA,GU);; GU,SA);; + GS,GS);; OB,OB);; NO,NO);; *) echo "Incompatible results: $resx,$resy"; exit 1;;