state_space

bounding_box(primes: dict, subspaces: List[Union[dict, str]]) Dict[str, int]

Returns the smallest subspace that contains the union of subspaces.

arguments:
  • primes: prime implicants

returns:
  • box: the smallest subspace that contains the union of subspaces

example:

>>> subspaces = [{"v1": 0, "v2": 0}, {"v1": 1, "v2": 0})]
>>> bounding_box(primes, subspaces)
{"v2": 0}
enumerate_states(primes: dict, proposition: str)

Generates all states that are referenced by proposition in the context of the variables given by primes. The syntax of proposition should be as in bnet files and TRUE and FALSE in will be treated as 1 and 0.

Note

This function uses bnet2primes and list_states_in_subspace to enumerate the states referenced by an expression. The efficiency of this approach can decreases a lot starting from around 15 variables that appear in proposition.

arguments:
  • primes: prime implicants

  • proposition: a propositional formula

returns:
  • states: the referenced states in str format

example:

>>> prop = "!Erk | (Raf & Mek)"
>>> enumerate_states(primes,prop)[0]
"010"
find_vanham_variables(primes: dict) Dict[int, List[str]]

Detects variables that represent multi-valued variables using the Van Ham encoding, see Didier2011 for more details. E.g. three-valued variables x are encoded via two Boolean variables x_medium and x_high. This function is used for example by ModelChecking.primes2smv to add INIT constraints to the smv file that forbid all states that are not admissible, e.g. in which “!x_medium & x_high” is true.

arguments:
  • primes: prime implicants

returns:
  • names: activity levels and names

example:

>>> find_vanham_variables(primes)
{2: ['E2F1', 'ATM'],
 3: ['ERK'],
 4: [],
 5: []}
hamming_distance(this: dict, other: dict) int

Returns the Hamming distance between to subspaces. Variables that are free in either subspace are ignored.

arguments:
  • this, other: subspaces in dictionary representation

returns:
  • distance: the distance between Subspace1 and Subspace2

example:

>>> hamming_distance({"v1":0,"v2":0}, {"v1":1,"v2":1})
2
>>> hamming_distance({"v1":1}, {"v2":0})
0
is_subspace(primes: dict, this: ~typing.Union[dict, str], other: [<class 'dict'>, <class 'str'>]) bool

Checks whether this is a subspace of other.

arguments:
  • primes: prime implicants

  • this: a subspace

  • other: a subspace

returns:
  • answer: whether this is subspace of other

example:

>>> is_subspace(primes, this=sub1, other=sub2)
True
list_states_in_subspace(primes: dict, subspace)

Generates all states contained in subspace.

arguments:
  • primes: prime implicants or a list of names

  • subspace: a subspace

returns:
  • states: the states contained in subspace

example:

>>> subspace = "1-1"
>>> list_states_in_subspace(primes,subspace)
['101','111']
random_state(primes: dict, subspace: Union[dict, str] = {}) dict

Generates a random state of the transition system defined by primes. If subspace is given then the state will be drawn from that subspace.

arguments:
  • primes: prime implicants

  • subspace: a subspace

returns:
  • state: random state inside subspace

example:

>>> random_state(primes)
{'v1':1, 'v2':1, 'v3':1}
>>> random_state(primes, {"v1":0})
{'v1':0, 'v2':1, 'v3':0}
>>> random_state(primes, "0--")
{'v1':0, 'v2':0, 'v3':1}
size_state_space(primes: dict, van_ham: bool = True, fixed_inputs: bool = False)

This function computes the number of states in states space of primes. Detects if there are variables that encode multi-valued variables via the Van Ham encoding. Variables that have the same name module the Van Ham extension (see example below) are identified. E.g. the state space of x_medium, x_high is 3 instead of 4 since “!x_medium & x_high” is not an admissible state, see Didier2011 for more details.

arguments:
  • primes: prime implicants

  • van_ham: exclude states that are not admissible in Van Ham encoding

  • fixed_inputs: return number of states for single input combination

returns:
  • size: number of states

example:

>>> StateTransitionGraphs.VAN_HAM_EXTENSIONS
["_medium", "_high", "_level1", "_level2", "_level3", "_level4", "_level5"]
>>> size_state_space(primes, van_ham=False)
256
>>> size_state_space(primes)
192
>>> size_state_space(primes, fixed_inputs=True)
96
state2dict(primes: dict, state) dict

Converts the string representation of a state into the dictionary representation of a state. If state is already of type dict it is simply returned.

arguments
  • primes: prime implicants or a list of names

  • state: string representation of state

returns
  • state: dictionary representation of state

example:

>>> state = "101"
>>> state2dict(primes, state)
{'v2':0, 'v1':1, 'v3':1}
state2str(state: Union[dict, str]) str

Converts the dictionary representation of a state into the string representation of a state. If state is already of type string it is simply returned.

arguments
  • state: dictionary representation of state

returns
  • state: string representation of state

example:

>>> state = {"v2":0, "v1":1, "v3":1}
>>> state2str(primes, state)
'101'
state_is_in_subspace(primes: dict, state: Union[str, dict], subspace: Union[str, dict]) bool

Checks whether state is a state in subspace.

arguments:
  • primes: prime implicants

  • state: a state

  • subspace: a subspace

returns:
  • answer: whether state is a state in subspace

example:

>>> state_is_in_subspace(primes, state, subspace)
False
states2dict(primes: dict, states: List[str]) List[dict]

Converts the string representation of a list of states into the dictionary representations. If state is already of type dict it is simply returned.

arguments
  • primes: prime implicants or a list of names

  • states: string representation of states

returns
  • states: dictionary representation of states

example:

>>> states = ["101", "100"]
>>> states2dict(primes, state)
[{'v2':0, 'v1':1, 'v3':1},{'v2':0, 'v1':1, 'v3':0}]
states2str(primes: dict, states: List[dict]) List[str]

Converts the string representation of a list of states into the dictionary representations. If state is already of type dict it is simply returned.

arguments
  • primes: prime implicants or a list of names

  • states: dictionary representation of states

returns
  • states: string representation of states

example:

>>> states = [{'v2':0, 'v1':1, 'v3':1},{'v2':0, 'v1':1, 'v3':0}]
>>> states2str(primes, state)
["101", "100"]
subspace2dict(primes: dict, subspace)

Converts the string representation of a subspace into the dictionary representation of a subspace. Use “-” to indicate free variables. If subspace is already of type dict it is simply returned.

arguments
  • primes: prime implicants or a list of names

  • subspace: a subspace

returns
  • subspace: the dictionary representation of subspace

example:

>>> sub = "-01"
>>> subspace2dict(primes, sub)
{'v2':0, 'v3':1}
subspace2str(primes: dict, subspace)

Converts the dictionary representation of a subspace into the string representation of a subspace. Uses “-” to indicate free variables. If subspace is already of type str it is simply returned.

arguments
  • primes: prime implicants or a list of names

  • subspace: a subspace

returns
  • subspace: the string representation of subspace

example:

>>> sub = {"v2":0, "v3":1}
>>> subspace2str(primes, sub)
'-01'