From a4a0cf3bb251749562deff2dba4cd93ddcb2e2e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 27 Jan 2015 10:21:17 +0100 Subject: [PATCH] ltl: keep track of spin-compatible AP * src/misc/bareword.cc, src/misc/bareword.hh (is_spin_ap): New function. * src/ltlast/formula.cc, src/ltlast/formula.hh (is_spin_atomic_props): New method and boolean. * src/ltlast/atomic_prop.cc, src/ltlast/constant.cc: Update it. * src/ltltest/kind.test: Test it. --- src/ltlast/atomic_prop.cc | 9 +- src/ltlast/constant.cc | 4 + src/ltlast/formula.cc | 5 +- src/ltlast/formula.hh | 6 ++ src/ltltest/kind.test | 204 +++++++++++++++++++------------------- src/misc/bareword.cc | 14 ++- src/misc/bareword.hh | 9 +- 7 files changed, 143 insertions(+), 108 deletions(-) diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index c4ad4b034..139be1f6e 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -23,6 +23,7 @@ #include "config.h" #include "atomic_prop.hh" #include "visitor.hh" +#include "misc/bareword.hh" #include #include #include @@ -60,12 +61,14 @@ namespace spot // is.lbt_atomic_props should be true if the name has the form // pNN where NN is any number of digit. std::string::const_iterator pos = name.begin(); - is.lbt_atomic_props = (pos != name.end() && *pos++ == 'p'); - while (is.lbt_atomic_props && pos != name.end()) + bool lbtap = (pos != name.end() && *pos++ == 'p'); + while (lbtap && pos != name.end()) { char l = *pos++; - is.lbt_atomic_props = (l >= '0' && l <= '9'); + lbtap = (l >= '0' && l <= '9'); } + is.lbt_atomic_props = lbtap; + is.spin_atomic_props = lbtap || is_spin_ap(name.c_str()); } atomic_prop::~atomic_prop() diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 57fde76e6..409c47f40 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -59,6 +59,8 @@ namespace spot is.syntactic_persistence = true; is.not_marked = true; is.accepting_eword = false; + is.lbt_atomic_props = true; + is.spin_atomic_props = true; break; case constant::EmptyWord: is.boolean = false; @@ -80,6 +82,8 @@ namespace spot is.universal = false; is.not_marked = true; is.accepting_eword = true; + is.lbt_atomic_props = true; + is.spin_atomic_props = true; break; } } diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index 52ab7b8b4..c2b92f52b 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -56,7 +56,10 @@ namespace spot proprint(is_syntactic_recurrence, "r", "syntactic recurrence"); \ proprint(is_marked, "+", "marked"); \ proprint(accepts_eword, "0", "accepts the empty word"); \ - proprint(has_lbt_atomic_props, "l", "has LBT-style atomic props"); + proprint(has_lbt_atomic_props, "l", \ + "has LBT-style atomic props"); \ + proprint(has_spin_atomic_props, "a", \ + "has Spin-style atomic props"); std::list diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index b7903e193..03f36d041 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -293,6 +293,11 @@ namespace spot return is.lbt_atomic_props; } + bool has_spin_atomic_props() const + { + return is.spin_atomic_props; + } + /// The properties as a field of bits. For internal use. unsigned get_props() const { @@ -354,6 +359,7 @@ namespace spot bool not_marked:1; // No occurrence of EConcatMarked. bool accepting_eword:1; // Accepts the empty word. bool lbt_atomic_props:1; // Use only atomic propositions like p42. + bool spin_atomic_props:1; // Use only spin-compatible atomic props. }; union { diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index e7dc64ff5..603c58a9c 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -26,110 +26,110 @@ set -e cat >input<b,BxfLEPSFsgopr -!a,B&!xfLEPSFsgopr -!(a|b),B&xfLEPSFsgopr -F(a),&!xLPegopr -G(a),&!xLPusopr -a U b,&!xfLPgopr -a U Fb,&!xLPegopr -Ga U b,&!xLPopr -1 U a,&!xfLPegopr -a W b,&!xfLPsopr -a W 0,&!xfLPusopr -a M b,&!xfLPgopr -a M 1,&!xfLPegopr -a R b,&!xfLPsopr -0 R b,&!xfLPusopr -a R (b R (c R d)),&!xfLPsopr -a U (b U (c U d)),&!xfLPgopr -a W (b W (c W d)),&!xfLPsopr -a M (b M (c M d)),&!xfLPgopr -Fa -> Fb,xLPopr -Ga -> Fb,xLPgopr -Fa -> Gb,xLPsopr -(Ga|Fc) -> Fb,xLPopr -(Ga|Fa) -> Gb,xLPopr -{a;c*;b}|->!Xb,&fPsopr -{a;c*;b}|->X!b,&!fPsopr -{a;c*;b}|->!Fb,&Psopr -{a;c*;b}|->G!b,&!Psopr -{a;c*;b}|->!Gb,&Pr -{a;c*;b}|->F!b,&!Pr -{a;c*;b}|->GFa,&!Pr -{a;c*;b}|->FGa,&!P -{a[+];c[+];b*}|->!Fb,&xPsopr -{a[+];c*;b[+]}|->G!b,&!xPsopr -{a*;c[+];b[+]}|->!Gb,&xPr -{a[+];c*;b[+]}|->F!b,&!xPr -{a[+];c[+];b*}|->GFa,&!xPr -{a*;c[+];b[+]}|->FGa,&!xP -{a;c;b|(d;e)}|->!Xb,&fPFsgopr -{a;c;b|(d;e)}|->X!b,&!fPFsgopr -{a;c;b|(d;e)}|->!Fb,&Psopr -{a;c;b|(d;e)}|->G!b,&!Psopr -{a;c;b|(d;e)}|->!Gb,&Pgopr -{a;c;b|(d;e)}|->F!b,&!Pgopr -{a;c;b|(d;e)}|->GFa,&!Pr -{a;c;b|(d;e)}|->FGa,&!Pp -{a[+] && c[+]}|->!Xb,&fPsopr -{a[+] && c[+]}|->X!b,&!fPsopr -{a[+] && c[+]}|->!Fb,&xPsopr -{a[+] && c[+]}|->G!b,&!xPsopr -{a[+] && c[+]}|->!Gb,&xPr -{a[+] && c[+]}|->F!b,&!xPr -{a[+] && c[+]}|->GFa,&!xPr -{a[+] && c[+]}|->FGa,&!xP -{a;c*;b}<>->!Gb,&Pgopr -{a;c*;b}<>->F!b,&!Pgopr -{a;c*;b}<>->FGb,&!Pp -{a;c*;b}<>->!GFb,&Pp -{a;c*;b}<>->GFb,&!P -{a;c*;b}<>->!FGb,&P -{a*;c[+];b[+]}<>->!FGb,&xP -{a;c|d;b}<>->!Gb,&Pgopr -{a;c|d;b}<>->G!b,&!Psopr -{a;c|d;b}<>->FGb,&!Pp -{a;c|d;b}<>->!GFb,&Pp -{a;c|d;b}<>->GFb,&!Pr -{a;c|d;b}<>->!FGb,&Pr +a,B&!xfLEPSFsgopra +a<->b,BxfLEPSFsgopra +!a,B&!xfLEPSFsgopra +!(a|b),B&xfLEPSFsgopra +F(a),&!xLPegopra +G(a),&!xLPusopra +a U b,&!xfLPgopra +a U Fb,&!xLPegopra +Ga U b,&!xLPopra +1 U a,&!xfLPegopra +a W b,&!xfLPsopra +a W 0,&!xfLPusopra +a M b,&!xfLPgopra +a M 1,&!xfLPegopra +a R b,&!xfLPsopra +0 R b,&!xfLPusopra +a R (b R (c R d)),&!xfLPsopra +a U (b U (c U d)),&!xfLPgopra +a W (b W (c W d)),&!xfLPsopra +a M (b M (c M d)),&!xfLPgopra +Fa -> Fb,xLPopra +Ga -> Fb,xLPgopra +Fa -> Gb,xLPsopra +(Ga|Fc) -> Fb,xLPopra +(Ga|Fa) -> Gb,xLPopra +{a;c*;b}|->!Xb,&fPsopra +{a;c*;b}|->X!b,&!fPsopra +{a;c*;b}|->!Fb,&Psopra +{a;c*;b}|->G!b,&!Psopra +{a;c*;b}|->!Gb,&Pra +{a;c*;b}|->F!b,&!Pra +{a;c*;b}|->GFa,&!Pra +{a;c*;b}|->FGa,&!Pa +{a[+];c[+];b*}|->!Fb,&xPsopra +{a[+];c*;b[+]}|->G!b,&!xPsopra +{a*;c[+];b[+]}|->!Gb,&xPra +{a[+];c*;b[+]}|->F!b,&!xPra +{a[+];c[+];b*}|->GFa,&!xPra +{a*;c[+];b[+]}|->FGa,&!xPa +{a;c;b|(d;e)}|->!Xb,&fPFsgopra +{a;c;b|(d;e)}|->X!b,&!fPFsgopra +{a;c;b|(d;e)}|->!Fb,&Psopra +{a;c;b|(d;e)}|->G!b,&!Psopra +{a;c;b|(d;e)}|->!Gb,&Pgopra +{a;c;b|(d;e)}|->F!b,&!Pgopra +{a;c;b|(d;e)}|->GFa,&!Pra +{a;c;b|(d;e)}|->FGa,&!Ppa +{a[+] && c[+]}|->!Xb,&fPsopra +{a[+] && c[+]}|->X!b,&!fPsopra +{a[+] && c[+]}|->!Fb,&xPsopra +{a[+] && c[+]}|->G!b,&!xPsopra +{a[+] && c[+]}|->!Gb,&xPra +{a[+] && c[+]}|->F!b,&!xPra +{a[+] && c[+]}|->GFa,&!xPra +{a[+] && c[+]}|->FGa,&!xPa +{a;c*;b}<>->!Gb,&Pgopra +{a;c*;b}<>->F!b,&!Pgopra +{a;c*;b}<>->FGb,&!Ppa +{a;c*;b}<>->!GFb,&Ppa +{a;c*;b}<>->GFb,&!Pa +{a;c*;b}<>->!FGb,&Pa +{a*;c[+];b[+]}<>->!FGb,&xPa +{a;c|d;b}<>->!Gb,&Pgopra +{a;c|d;b}<>->G!b,&!Psopra +{a;c|d;b}<>->FGb,&!Ppa +{a;c|d;b}<>->!GFb,&Ppa +{a;c|d;b}<>->GFb,&!Pra +{a;c|d;_b}<>->!FGb,&Pr # Equivalent to a&b&c&d -{a:b:c:d}!,B&!xfLEPSFsgopr -a&b&c&d,B&!xfLEPSFsgopr -(Xa <-> XXXc) U (b & Fe),LPgopr -(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopr -(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopr -(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopr -(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopr -(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPp -(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPr -(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPp -(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b)),LPup -(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPr -(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b)),LPer -(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPep -(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb)),LP -(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPur -(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb)),LP -GFa M GFb,&!xLPeu -FGa M FGb,&!xLPeup -Fa M GFb,&!xLPer -GFa W GFb,&!xLPeur -FGa W FGb,&!xLPeu -Ga W FGb,&!xLPup -Ga W b,&!xLPsopr -Fa M b,&!xLPgopr -{a;b*;c},&!fPsopr -{a;b*;c}!,&!fPgopr +{a:b:c:d}!,B&!xfLEPSFsgopra +a&b&c&d,B&!xfLEPSFsgopra +(Xa <-> XXXc) U (b & Fe),LPgopra +(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopra +(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopra +(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopra +(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopra +(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPpa +(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPra +(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPpa +(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b)),LPupa +(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPra +(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b)),LPera +(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPepa +(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb)),LPa +(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPura +(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb)),LPa +GFa M GFb,&!xLPeua +FGa M FGb,&!xLPeupa +Fa M GFb,&!xLPera +GFa W GFb,&!xLPeura +FGa W FGb,&!xLPeua +Ga W FGb,&!xLPupa +Ga W b,&!xLPsopra +Fa M b,&!xLPgopra +{a;b*;c},&!fPsopra +{a;b*;c}!,&!fPgopra # The negative normal form is {a;b*;c}[]->1 -!{a;b*;c}!,&fPsopr -{a;b*;c}[]->0,&!fPsopr -!{a;b*;c},&!fPgopr -!{a[+];b*;c[+]},&!xfPgopr -{a[+];b*;c[+]},&!xfPsopr -{a[+] && b || c[+]},&!fPsopr -{a[+] && b[+] || c[+]},&!xfPsopr +!{a;b*;c}!,&fPsopra +{a;b*;p112}[]->0,&!fPsopra +!{a;b*;c.2},&!fPgopr +!{a[+];b*;c[+]},&!xfPgopra +{a[+];b*;c[+]},&!xfPsopra +{a[+] && b || c[+]},&!fPsopra +{a[+] && b[+] || c[+]},&!xfPsopra EOF run 0 ../kind input diff --git a/src/misc/bareword.cc b/src/misc/bareword.cc index d154c04e0..4076d9b64 100644 --- a/src/misc/bareword.cc +++ b/src/misc/bareword.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2011, 2013, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -50,4 +50,16 @@ namespace spot return "\"" + escape_str(str) + "\""; } + // This is for Spin 5. Spin 6 has a relaxed parser that can + // accept any parenthesized block as an atomic propoistion. + bool is_spin_ap(const char* str) + { + if (!str || !islower(*str)) + return false; + while (*++str) + if (!(isalnum(*str) || *str == '_')) + return false; + return true; + } + } diff --git a/src/misc/bareword.hh b/src/misc/bareword.hh index 735c16100..d5bbefc4e 100644 --- a/src/misc/bareword.hh +++ b/src/misc/bareword.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -40,6 +40,13 @@ namespace spot /// \brief Double-quote words that are not bare. /// \see is_bare_word SPOT_API std::string quote_unless_bare_word(const std::string& str); + + /// \brief Whether a word can be used as an atomic proposition for Spin 5. + /// + /// In Spin 5 (hence in ltl2ba and ltl3ba as well) atomic + /// propositions should start with a lowercase letter, and can then + /// consist solely of alphanumeric characters and underscores. + SPOT_API bool is_spin_ap(const char* str); /// @} }