Planner Synthesis

Jtlvint Module — Interface to JTLV

About JTLV, see http://jtlv.ysaar.net/

jtlvint.checkRealizability(smv_file='', spc_file='', aut_file='', heap_size='-Xmx128m', pick_sys_init=True, file_exist_option='a', verbose=0)

Determine whether the spec in smv_file and spc_file is realizable without extracting an automaton.

Input:

• smv_file: a string that specifies the name of the smv file.
• spc_file: a string that specifies the name of the spc file.
• aut_file: a string that specifies the name of the file containing the output of JTLV (e.g. an initial state starting from which the spec is cannot be satisfied).
• heap_size: a string that specifies java heap size.
• pick_sys_init is a boolean indicating whether the system can pick its initial state (in response to the initial environment state).
• file_exist_option: a string that indicate what to do when the specified aut_file exists. Possible values are: ‘a’ (ask whether to replace or create a new file), ‘r’ (replace the existing file), ‘n’ (create a new file).
• verbose: an integer that specifies the level of verbosity.

jtlvint.computeStrategy(smv_file, spc_file, aut_file='', heap_size='-Xmx128m', priority_kind=3, init_option=1, file_exist_option='a', verbose=0)

Compute an automaton satisfying the spec in smv_file and spc_file and store in aut_file. Return the realizability of the spec.

Input:

• smv_file: a string that specifies the name of the smv file.

• spc_file: a string that specifies the name of the spc file.

• aut_file: a string that specifies the name of the file containing the resulting automaton.

• 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:

  • 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 in 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.

• file_exist_option: a string that indicate what to do when the specified aut_file exists. Possible values are: ‘a’ (ask whether to replace or create a new file), ‘r’ (replace the existing file), ‘n’ (create a new file).

• verbose: an integer that specifies the level of verbosity.

jtlvint.generateJTLVInput(env_vars={}, sys_disc_vars={}, spec=[], disc_props={}, disc_dynamics=<prop2part.PropPreservingPartition instance at 0x105ac4518>, smv_file='tmp.smv', spc_file='tmp.spc', file_exist_option='a', verbose=0)

Generate JTLV input files: smv_file and spc_file.

Input:

• env_vars: a dictionary {str : str} or {str : list} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, ..., 5} or [0, 2, 3, 4, 5].
• sys_disc_vars: a dictionary {str : str} or {str : list} whose keys are the names of discrete system variables and whose values are their possible values.
• spec: a list of two strings that represents system specification of the form assumption -> guarantee; the first string is the assumption and the second string is the guarantee.
• disc_props: a dictionary {str : str} whose keys are the symbols for propositions on discrete variables and whose values are the actual propositions on discrete variables.
• disc_dynamics: a PropPreservingPartition object that represents the transition system obtained from the discretization procedure.
• smv_file: a string that specifies the name of the resulting smv file.
• spc_file: a string that specifies the name of the resulting spc file.
• file_exist_option: a string that indicate what to do when the specified smv_file or spc_file exists. Possible values are: ‘a’ (ask whether to replace or create a new file), ‘r’ (replace the existing file), ‘n’ (create a new file).
• verbose: an integer that specifies the level of verbosity. If verbose is set to 0, this function will not print anything on the screen.

jtlvint.getCounterExamples(aut_file, verbose=0)

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

Input:

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

jtlvint.setJTLVExe(jtlv_exe)

Set the name of the jtlv executable.

Input:

• jtlv_exe: a string indicating the name of the executable jar containing the jtlv GR1 game implementation.

jtlvint.setJTLVPath(jtlv_path)

Set path to jtlv_grgame.jar.

Input:

• jtlv_path: a string indicating the full path to the JTLV folder.

jtlvint.solveGame(smv_file, spc_file, aut_file='', heap_size='-Xmx128m', priority_kind=3, init_option=1, file_exist_option='a', verbose=0)

Compute an automaton satisfying the spec in smv_file and spc_file and store in aut_file. Return the realizability of the spec.

Input:

• smv_file: a string that specifies the name of the smv file.

• spc_file: a string that specifies the name of the spc file.

• aut_file: a string that specifies the name of the file containing the resulting automaton.

• 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:

  • 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 in 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.

• file_exist_option: a string that indicate what to do when the specified aut_file exists. Possible values are: ‘a’ (ask whether to replace or create a new file), ‘r’ (replace the existing file), ‘n’ (create a new file).

• verbose: an integer that specifies the level of verbosity.

jtlvint.synthesize(env_vars={}, sys_disc_vars={}, spec='', disc_props={}, disc_dynamics=<prop2part.PropPreservingPartition instance at 0x105ac4098>, smv_file='tmp.smv', spc_file='tmp.spc', aut_file='', heap_size='-Xmx128m', priority_kind=3, init_option=1, file_exist_option='a', verbose=0)

Compute an automaton satisfying spec. Return the realizability of spec.

If spec is realizable, the resulting automaton will be stored in the aut_file. Otherwise, the counter examples will be stored. This function essentially combines generateJTLVInput and computeStrategy

Input:

• env_vars: a dictionary {str : str} or {str : list} whose keys are the names of environment variables and whose values are their possible values, e.g., boolean or {0, 2, ..., 5} or [0, 2, 3, 4, 5].
• sys_disc_vars: a dictionary {str : str} or {str : list} whose keys are the names of discrete system variables and whose values are their possible values.
• spec: a list of two strings that represents system specification of the form assumption -> guarantee; the first string is the assumption and the second string is the guarantee.
• disc_props: a dictionary {str : str} whose keys are the symbols for propositions on discrete variables and whose values are the actual propositions on discrete variables.
• disc_dynamics: a PropPreservingPartition object that represents the transition system obtained from the discretization procedure.
• smv_file: a string that specifies the name of the resulting smv file.
• spc_file: a string that specifies the name of the resulting spc file.
• aut_file: a string that specifies the name of the file containing the resulting automaton.
• 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. See the documentation of the computeStrategy function for the possible values of priority_kind.
• init_option: an integer in that specifies how to handle the initial state of the system. See the documentation of the computeStrategy function for the possible values of init_option.
• file_exist_option: a string that indicate what to do when the specified smv_file or spc_file exists. Possible values are: ‘a’ (ask whether to replace or create a new file), ‘r’ (replace the existing file), ‘n’ (create a new file).
• verbose: an integer that specifies the level of verbosity. If verbose is set to 0, this function will not print anything on the screen.

Automaton Module

class automaton.Automaton(states_or_file=[], varnames=[], verbose=0)

Automaton class for representing a finite state automaton. An Automaton object contains the following field:

• states: a list of AutomatonState objects.

Automaton([states_or_file, varname, verbose]) constructs an Automaton object based on the following input:

• states_or_file: a string containing the name of the aut file to be loaded or a list of AutomatonState objects to be assigned to the states of this Automaton object, or an (open) file-like object.
• varname: a list of all the variable names. If it is not empty and states_or_file is a string representing the name of the aut file to be loaded, then this function will also check whether the variables in aut_file are in varnames.

addAutState(aut_state)

Add an AutomatonState object to this automaton.

Input:

• aut_state: an AutomatonState object to be added to this Automaton object.

copy()

Return copy of this Automaton.

createPygraphRepr()

Generate a python-graph representation of this automaton, stored in ‘self.pygraph’

dumpXML(pretty=True, idt_level=0)

Return string of automaton conforming to tulipcon XML.

If pretty is True, then use indentation and newlines to make the resulting XML string more visually appealing. idt_level is the base indentation level on which to create automaton string. This level is only relevant if pretty=True.

Note that name subtags within aut tag are left blank.

findAllAutPartState(state_frag)

Return list of nodes consistent with the given fragment.

state_frag should be a dictionary. We say the state in a node is ``consistent’’ with the fragment if for every variable appearing in state_frag, the valuations in state_frag and the node are the same.

E.g., let aut be an instance of Automaton. Then aut.findAllAutPartState({“foobar” : 1}) would return a list of nodes (instances of AutomatonState) in which the variable “foobar” is 1 (true).

findAllAutState(state)

Return all the AutomatonState objects stored in this automaton whose state matches state. Return -1 if such an AutomatonState objects is not found.

Input:

• state: a dictionary whose keys are the names of the variables and whose values are the values of the variables.

findAutState(state)

Return the first AutomatonState object stored in this automaton whose state matches state. Return -1 if such an AutomatonState objects is not found.

Input:

• state: a dictionary whose keys are the names of the variables and whose values are the values of the variables.

findNextAutState(current_aut_state, env_state={}, deterministic_env=True)

Return the next AutomatonState object based on env_state. Return -1 if such an AutomatonState object is not found.

Input:

• current_aut_state: the current AutomatonState. Use current_aut_state = None for unknown current or initial automaton state.
• env_state: a dictionary whose keys are the names of the environment variables and whose values are the values of the variables.
• ‘deterministic_env’: specifies whether to choose the environment state deterministically.

getAutInSet(aut_state_id)

Find all nodes that include given ID in their outward transitions.

If the automaton is viewed as a directed graph, and the given ID corresponds to node v, then we are interested in all v’in V such that (v’,v) is an edge in the graph.

(Comments on efficiency.) The automaton is stored as a tree, where parents connect to children as in a linked list. Thus given a node, finding the set of outward edges takes constant time, whereas finding the inward set (as done by this method) requires searching the set of nodes and their respective transition sets; so, O(N*M) time, where N is the number of nodes and M is the average number of outward edges.

Return list of nodes (instances of AutomatonState), or None on error.

getAutInit()

Return list of nodes that are initial, i.e., have empty In set.

N.B., the set of initial nodes is not saved, so every time you call getAutInit, all nodes are checked for empty inward edge sets, which itself incurs a search cost (cf. doc for method getAutInSet).

getAutState(aut_state_id)

Return an AutomatonState object stored in this Automaton object whose id is aut_state_id. Raise IndexError if such AutomatonState object does not exist.

Input:

• aut_state_id: an integer specifying the id of the AutomatonState object to be returned by this function.

loadFile(aut_file, varnames=[], verbose=0)

Construct an automation from aut_file.

Input:

• aut_file: the name of the text file containing the automaton, or an (open) file-like object.
• varnames: a list of all the variable names. If it is not empty, then this function will also check whether the variables in aut_file are in varnames.

loadPygraphRepr()

Recreate automaton states from ‘self.pygraph’.

Merge and update transition listings as needed. N.B., this method will change IDs after trimming to ensure indexing still works (since self.states attribute is a list).

loadXML(x, namespace='')

Read an automaton from given string conforming to tulipcon XML.

N.B., on a successful processing of the given string, the original Automaton instance to which this method is attached is replaced with the new structure. On failure, however, the original Automaton is untouched.

The argument x can also be an instance of xml.etree.ElementTree._ElementInterface ; this is mainly for internal use, e.g. by the function untagpolytope and some load/dumpXML methods elsewhere.

Return True on success; on failure, return False or raise exception.

setAutStateState(aut_state_id, aut_state_state, verbose=0)

Set the state of the AutomatonState object whose id is aut_state_id to aut_state_state. If such an AutomatoSstate object does not exist, an AutomatonState object whose id is aut_state_id and whose state is aut_state_state will be added.

Input:

• aut_state_id: an integer that specifies the id of the AutomatonState object to be set.
• aut_state_state: a dictionary that represents the new state of the AutomatonState object.

setAutStateTransition(aut_state_id, aut_state_transition, verbose=0)

Set the transition of the AutomatonState object whose id is aut_state_id to aut_state_transition. If such automaton state does not exist, an AutomatonState whose id is aut_state_id and whose transition is aut_state_transition will be added.

Input:

• aut_state_id: an integer that specifies the id of the AutomatonState object to be set.
• aut_state_transition: a list of id’s of the AutomatonState objects to which the AutomatonState object with id aut_state_id can transition.

trimDeadStates()

Recursively delete states with no outgoing transitions.

Merge and update transition listings as needed. N.B., this method will change IDs after trimming to ensure indexing still works (since self.states attribute is a list).

trimRedundantStates()

DEFUNCT UNTIL FURTHER NOTICE!

Combine states whose valuation of variables is identical

Merge and update transition listings as needed. N.B., this method will change IDs after trimming to ensure indexing still works (since self.states attribute is a list).

Return False on failure; True otherwise (success).

trimUnconnectedStates(aut_state_id)

Delete all states that are inaccessible from the given state.

Merge and update transition listings as needed. N.B., this method will change IDs after trimming to ensure indexing still works (since self.states attribute is a list).

writeDotFile(fname, hideZeros=False, distinguishTurns=None, turnOrder=None)

Write automaton to Graphviz DOT file.

In each state, the node ID and nonzero variables and their value (in that state) are listed. This style is motivated by Boolean variables, but applies to all variables, including those taking arbitrary integer values.

N.B., to allow for trace memory (manifested as ``rank’’ in JTLV output), we include an ID for each node. Thus, identical valuation of variables does not imply state equivalency (confusingly).

If hideZeros is True, then for each vertex (in the DOT diagram) variables taking the value 0 are not shown. This may lead to more succinct diagrams when many boolean variables are involved. The default if False, i.e. show all variable values.

It is possible to break states into a linear sequence of steps for visualization purposes using the argument distinguishTurns. If not None, distinguishTurns should be a dictionary with keys as strings indicating the agent (e.g. “env” and “sys”), and values as lists of variable names that belong to that agent. These lists should be disjoint. Note that variable names are case sensitive!

If distinguishTurns is not None, state labels (in the DOT digraph) now have a preface of the form ID::agent, where ID is the original state identifier and “agent” is a key from distinguishTurns.

N.B., if distinguishTurns is not None and has length 1, it is ignored (i.e. treated as None).

turnOrder is only applicable if distinguishTurns is not None. In this case, if turnOrder is None, then use whatever order is given by default when listing keys of distinguishTurns. Otherwise, if turnOrder is a list (or list-like), then each element is key into distinguishTurns and state decompositions take that order.

Return False on failure; True otherwise (success).

writeDotFileEdged(fname, env_vars, sys_vars, hideZeros=False, hideAgentNames=True)

Write edge-labeled automaton to Graphviz DOT file.

I forked the method writeDotFile for fear of feature creep. At least now the features will creep upon us from separate methods, rather than a single complicated argument list.

env_vars and sys_vars should be lists of variable names (type string) describing environment and system variables, respectively.

The intent is to view nodes labeled with a system decision, and edges labeled with an environment decision, thus better expressing the game. Recall the automaton is a strategy.

Return False on failure; True otherwise (success).

writeFile(destfile)

Write an aut file that is readable by ‘self.loadFile’. Note that this is not a true automaton file.

Input:

• ‘destfile’: the file name to be written to.

class automaton.AutomatonState(id=-1, state={}, transition=[])

AutomatonState class for representing a state in a finite state automaton. An AutomatonState object contains the following fields:

• id: an integer specifying the id of this AutomatonState object.
• state: a dictionary whose keys are the names of the variables and whose values are the values of the variables.
• transition: a list of id’s of the AutomatonState objects to which this AutomatonState object can transition.

copy()

Return copy of this automaton node.

automaton.createAut(aut_file, varnames=[], verbose=0)

Construct an automation from aut_file.

Input:

• aut_file: the name of the text file containing the automaton.
• varnames: a list of all the variable names. If it is not empty, then this function will also check whether the variables in aut_file are in varnames.