alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Report formulas that are both safety and guarantee.

Browse source 
* src/tgbatest/ltl2tgba.cc (-O): Report formulas that are both
safety and guarantee.
* src/tgbatest/obligation.test: Add cases.
This commit is contained in:
Alexandre Duret-Lutz 2011-01-27 21:41:04 +01:00
parent db124d02c0
commit c8140de9d6
3 changed files with 22 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-01-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2011-01-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Rename is_safety_automaton() as is_guarantee_automaton() and Rename is_safety_automaton() as is_guarantee_automaton() and

11
src/tgbatest/ltl2tgba.cc
View file

@ -1152,16 +1152,23 @@ main(int argc, char** argv)
} }
else 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, " std::cout << "this is a guarantee property (hence, "
<< "an obligation property)"; << "an obligation property)";
} }
else if (is_safety_mwdba(minimized)) else if (s && !g)
{ {
std::cout << "this is a safety property (hence, " std::cout << "this is a safety property (hence, "
<< "an obligation property)"; << "an obligation property)";
} }
else if (s && g)
{
std::cout << "this is a guarantee and a safety property"
<< " (and of course an obligation property)";
}
else else
{ {
std::cout << "this is an obligation property that is " std::cout << "this is an obligation property that is "

5
src/tgbatest/obligation.test
View file

@ -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(p->F(s&!z&X(!z U t)))
NO G(q->G(p->(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))))) 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 EOF
grok() grok()
@ -87,6 +90,7 @@ grok()
case $1 in case $1 in
"this is a safety property"*) echo SA;; "this is a safety property"*) echo SA;;
"this is a guarantee property"*) echo GU;; "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 an obligation property"*) echo OB;;
"this is not an obligation property"*) echo NO;; "this is not an obligation property"*) echo NO;;
*) echo XX;; *) echo XX;;
@ -107,6 +111,7 @@ while read exp f; do
case $resx,$resy in case $resx,$resy in
SA,GU);; SA,GU);;
GU,SA);; GU,SA);;
GS,GS);;
OB,OB);; OB,OB);;
NO,NO);; NO,NO);;
*) echo "Incompatible results: $resx,$resy"; exit 1;; *) echo "Incompatible results: $resx,$resy"; exit 1;;