Home       Trees       Indices       Help   
TuLiP
Package tulip :: Package spec :: Module gr1_fragment
[frames] | no frames]

Module gr1_fragment

Test if given formula belongs to an LTL fragment that is convertible to deterministic Buchi Automata (readily expressible in GR(1) ).

reference

  1. Andreas Morgenstern and Klaus Schneider, A LTL Fragment for GR(1)-Synthesis, in Proceedings First International Workshop on Interactions, Games and Protocols (iWIGP), Electronic Proceedings in Theoretical Computer Science (EPTCS), 50, pp. 33--45, 2011, http://doi.org/10.4204/EPTCS.50.3
Functions
 
check(formula)
Parse formula string and create abstract syntax tree (AST).
 
str_to_grspec(f)
Return `GRSpec` from LTL formula `f` as `str`.
 
split_gr1(f)
Return `dict` of GR(1) subformulae.
 
has_operator(u, g, operators)
GRSpec
stability_to_gr1(p, aux='aux')
Convert <>[] p to GR(1).
GRSpec
response_to_gr1(p, q, aux='aux')
Convert [](p -> <> q) to GR(1).
GRSpec
eventually_to_gr1(p, aux='aux')
Convert <> p to GR(1).
GRSpec
until_to_gr1(p, q, aux='aux')
Convert p U q to GR(1).
Variables
  logger = logging.getLogger(__name__)
  __package__ = None
hash(x)
Function Details

str_to_grspec(f)

  
Return `GRSpec` from LTL formula `f` as `str`.

Formula `f` must be in the form:

  A -> G

where each of A, G is a conjunction of terms: `B`, `[]C`, `[]<>B`.
For more details on `B, C`, see [split_gr1].

@type f: `str`
@rtype: [GRSpec]

split_gr1(f)

  
Return `dict` of GR(1) subformulae.

The formula `f` is assumed to be a conjunction of expressions
of the form:
  `B`, `[]C` or `[]<>B`
where:
  - `C` can contain "next"
  - `B` cannot contain "next"

@param f: temporal logic formula
@type f: `str` or AST

@return: conjunctions of formulae A, B as `str`, grouped by keys:
    `'init', 'G', 'GF'`
@rtype: `dict` of `str`: `list` of `str`

stability_to_gr1(p, aux='aux')

 

Convert <>[] p to GR(1).

Warning: This conversion is sound, but not complete. See p.2, [E10]

GR(1) form:

   !(aux) &&
   [](aux -> X aux) &&
   []<>(aux) &&

   [](aux -> p)
Parameters:
  • aux (str) - name to use for auxiliary variable
  • p (str)
Returns: GRSpec

response_to_gr1(p, q, aux='aux')

 

Convert [](p -> <> q) to GR(1).

GR(1) form:

   []<>(aux) &&

   []( (p && !q) -> X ! aux) &&
   []( (! aux && !q) -> X ! aux)
Parameters:
  • aux (str) - name to use for auxiliary variable
  • q (str)
  • p (str)
Returns: GRSpec

eventually_to_gr1(p, aux='aux')

 

Convert <> p to GR(1).

GR(1) form:

   !(aux) &&
   [](aux -> X aux) &&
   []<>(aux) &&

   []( (!p && !aux) -> X!(aux) )
Parameters:
  • aux (str) - name to use for auxiliary variable
  • p (str)
Returns: GRSpec

until_to_gr1(p, q, aux='aux')

 

Convert p U q to GR(1).

GR(1) form:

   (!q -> !aux) &&
   [](q -> aux)
   [](aux -> X aux) &&
   []<>(aux) &&

   []( (!aux && X(!q) ) -> X!(aux) ) &&
   [](!aux -> p)
Parameters:
  • aux (str) - name to use for auxiliary variable
  • p (str)
Returns: GRSpec

   Home       Trees       Indices       Help   
TuLiP
Generated by Epydoc 3.0.1 on Sat Nov 19 00:11:17 2016 http://epydoc.sourceforge.net