Home       Trees       Indices       Help   
TuLiP
Package tulip :: Package interfaces :: Module jtlv
[frames] | no frames]

Module jtlv

Interface to the JTLV implementation of GR(1) synthesis

Relevant links:

Functions
 
check_realizable(spec, heap_size='-Xmx128m', priority_kind=-1, init_option=1)
Decide realizability of specification defined by given GRSpec object.
 
solve_game(spec, fSMV, fLTL, fAUT, heap_size='-Xmx128m', priority_kind=3, init_option=1)
Decide realizability of specification.
 
synthesize(spec, heap_size='-Xmx128m', priority_kind=3, init_option=1)
Synthesize a strategy satisfying the specification.
 
create_files(spec)
Create temporary files for read/write by JTLV.
int
get_priority(priority_kind)
Validate and convert priority_kind to the corresponding integer.
 
call_jtlv(heap_size, fSMV, fLTL, fAUT, priority_kind, init_option)
Subprocess calls to JTLV.
str
canon_to_jtlv_domain(dom)
Convert an LTL or GRSpec variable domain to JTLV style.
str
generate_jtlv_smv(spec)
Return the SMV module definitions needed by JTLV.
 
generate_jtlv_ltl(spec)
Return LTL specification for JTLV.
networkx.DiGraph
jtlv_output_to_networkx(lines, spec)
Return a graph after parsing JTLV's output.
 
get_counterexamples(aut_file)
Return a list of dictionaries, each representing a counter example.
 
remove_comments(spec)
Remove comment lines from string.
 
check_vars(varNames)
Complain if any variable name is a number or not a string.
 
check_spec(spec, varNames)
Verify that all non-operators in "spec" are in the list of vars.
Variables
  logger = logging.getLogger(__name__)
  DEBUG_SMV_FILE = 'smv.txt'
  DEBUG_LTL_FILE = 'ltl.txt'
  DEBUG_AUT_FILE = 'aut.txt'
  smv_template = '\nMODULE main\n VAR\n e : env();\n ...
  ltl_template = '\nLTLSPEC\n(\n{a}\n);\n\nLTLSPEC\n(\n{g}\n);\n'
  __package__ = 'tulip.interfaces'
Function Details

check_realizable(spec, heap_size='-Xmx128m', priority_kind=-1, init_option=1)

 

Decide realizability of specification defined by given GRSpec object.

Returns:
True if realizable, False if not, or an error occurs.

solve_game(spec, fSMV, fLTL, fAUT, heap_size='-Xmx128m', priority_kind=3, init_option=1)

 

Decide realizability of specification.

Return True if realizable, False if not, or an error occurs. Automaton is extracted for file names by fAUT, unless priority_kind == -1

Parameters:
  • fSMV, fLTL, fAUT - file name for use with JTLV. This enables synthesize() to access them later on.
  • heap_size - a string that specifies java heap size.
  • priority_kind - a string of length 3 or an integer that specifies the type of priority used in extracting the automaton. Possible values of priority_kind are:
    • -1 - No Automaton
    • 3 - 'ZYX'
    • 7 - 'ZXY'
    • 11 - 'YZX'
    • 15 - 'YXZ'
    • 19 - 'XZY'
    • 23 - 'XYZ'

    Here X means that the controller tries to disqualify one of the environment assumptions, Y means that the controller tries to advance with a finite path to somewhere, and Z means that the controller tries to satisfy one of his guarantees.

  • init_option - an integer that specifies how to handle the initial state of the system. Possible values of init_option are:
    • 0 - The system has to be able to handle all the possible initial system states specified on the guarantee side of the specification.
    • 1 (default) - The system can choose its initial state, in response to the initial environment state. For each initial environment state, the resulting automaton contains exactly one initial system state, starting from which the system can satisfy the specification.
    • 2 - The system can choose its initial state, in response to the initial environment state. For each initial environment state, the resulting automaton contain all the possible initial system states, starting from which the system can satisfy the specification.
  • spec (GRSpec)

synthesize(spec, heap_size='-Xmx128m', priority_kind=3, init_option=1)

 

Synthesize a strategy satisfying the specification.

Arguments are described in documentation for solve_game.

Returns:
Return strategy as instance of networkx.DiGraph, or a list of counter-examples as returned by get_counterexamples.

get_priority(priority_kind)

 

Validate and convert priority_kind to the corresponding integer.

Parameters:
  • priority_kind (str or int) - a string of length 3 or integer as may be used when invoking solve_game. Check documentation there for possible values.
Returns: int
if given priority_kind is permissible, then return integer representation of it. Else, return default ("ZYX").

canon_to_jtlv_domain(dom)

 

Convert an LTL or GRSpec variable domain to JTLV style.

Parameters:
  • dom - a variable domain, as would be provided by the values in the output_variables attribute of spec.form.LTL or sys_vars of spec.form.GRSpec.
Returns: str
variable domain string, ready for use in an SMV file, as expected by the JTLV solver.

generate_jtlv_smv(spec)

 

Return the SMV module definitions needed by JTLV.

Raises exception if malformed GRSpec object is detected.

Parameters:
Returns: str
string conforming to SMV file format that JTLV expects.

generate_jtlv_ltl(spec)

 

Return LTL specification for JTLV.

Parameters:

jtlv_output_to_networkx(lines, spec)

 

Return a graph after parsing JTLV's output.

Parameters:
  • lines (list of str) - as loaded from file
  • spec (GRSpec)
Returns: networkx.DiGraph

get_counterexamples(aut_file)

 

Return a list of dictionaries, each representing a counter example.

Parameters:
  • aut_file - a string containing the name of the file containing the counter examples generated by JTLV.

Variables Details

smv_template

Value:
'''
MODULE main
    VAR
        e : env();
        s : sys();

MODULE env -- inputs
    VAR
...

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