synth.synthesize() tries to assign out of bounds values

[krooken]

When I try to synthesize a strategy with a variable defined as "player_turn": (1,2), I get an exception from synth.synthesize() stating:

  File "tulip-control\tulip\synth.py", line 1111, in synthesize
    return _synthesize(specs, solver, rm_deadends)
  File "tulip-control\tulip\synth.py", line 1139, in _synthesize
    return _trim_strategy(strategy, specs, rm_deadends=rm_deadends)
  File "tulip-control\tulip\synth.py", line 1155, in _trim_strategy
    ctrl = strategy2mealy(strategy, specs)
  File "tulip-control\tulip\synth.py", line 1290, in strategy2mealy
    mach.transitions.add(u, v, attr_dict=None, check=False, **d)
  File "tulip-control\tulip\transys\labeled_graphs.py", line 443, in add
    attr_dict=attr_dict, check=check, **attr)
  File "tulip-control\tulip\transys\labeled_graphs.py", line 974, in add_edge
    typed_attr.update(attr_dict)
  File "tulip-control\tulip\transys\mathset.py", line 787, in update
    self[key] = other[key]
  File "tulip-control\tulip\transys\mathset.py", line 774, in __setitem__
    raise ValueError(msg)
ValueError: key: player_turn, cannot be assigned value: 0
Admissible values are:
	{1, 2}

If I change to "player_turn": (0,3), I do not get that exception, but I also do not get a strategy.

If the specification is changed such that the variable range is shifted to start at zero, I do not get an exception, and I also get the expected correct strategy as a result. (The definition of the variable is changed to "player_turn": (0,1) and all specifications are modified accordingly.)

This behavior is a bit unexpected. Bounds should probably be treated the same way regardless of the actual values. However, I cannot tell for sure whether this is an error in TuLiP/omega/dd, or in my understanding of the same.

I am on commit ce54897 of tulip-control, omega version 0.3.1, and dd version 0.5.5.

omega warns that I am using autoref

`omega.symbolic.symbolic` failed to import `dd.cudd`.
Will use `dd.autoref`.

During debugging I found that "player_turn": (1,2) is represented by two bits in the BDDs, while "player_turn": (0,1) is represented by one bit. That feels reasonable, but it makes me think that maybe the handling of bounds in the BDDs does not work correctly. I am too unfamiliar with the code base to be able to debug any further, though.

Code to reproduce

The code that does not work:

#!/usr/bin/env python
"""Stick picking game."""

from tulip import spec
from tulip import synth

sticks = 7
max_moves = 3

# Specifications
# Environment variables and assumptions
# Formulae governing the model of player 2

env_vars = {
    'player_2_picks': (0, max_moves),
}

env_init = {
    'player_2_picks = 0',
}

env_safe = {
    # If there are remaining sticks and it is player 2's turn
    # (s)he has to pick at least one stick.
    '(sticks > 0 && player_turn = 2) -> (player_2_picks = 1 || player_2_picks = 2 || player_2_picks = 3)',

    # If there is no sticks left, or not player 2's turn
    # player 2 should not be picking any sticks.
    '(sticks = 0 || player_turn != 2) -> player_2_picks = 0',

    # Noone can pick more sticks than what is left.
    'player_2_picks <= sticks',
}

# System variables and guarantees
# Formulae governing the model of player 1, and picking sticks from the stack

sys_vars = {
    'player_1_picks': (0, max_moves),
    'player_turn': (1, 2),
    'sticks': (0, sticks),
}

sys_init = {
    'player_1_picks = 1 || player_1_picks = 2 || player_1_picks = 3',
    'player_turn = 1',
    'sticks = {sticks}'.format(sticks=sticks),
}

sys_safe = {
    # Model of player 1:

    # Same as for player 2
    "(sticks > 0 && player_turn = 1) -> (player_1_picks = 1 || player_1_picks = 2 || player_1_picks = 3)",

    # Same as for player 2
    "(sticks=0 || player_turn != 1) -> player_1_picks = 0",

    # Same as for player 2
    "player_1_picks <= sticks",

    # Model of the game:

    # If it is player 1's turn to pick, subtract her/his choice of
    # number of sticks from the stack.
    "player_turn = 1 -> sticks' = sticks-player_1_picks",

    # Same as previous, but for player 2.
    "player_turn = 2 -> sticks' = sticks-player_2_picks",

    # The turn is alternating while the game goes on (there are sticks left).
    "sticks > 0 -> (player_turn' != player_turn)",

    # Winning strategies for player 1:
    # (Choose one of the three)

    # Player 1 shall never pick all remaining sticks.
    # "(sticks > 0 && player_turn = 0) -> player_1_picks < sticks"

    # If the sticks are depleted during the next step,
    # then it should be caused by player 2's turn.
    # "(sticks > 0 && sticks' = 0) -> player_turn = 1"

    # If the sticks are depleted during the next step,
    # then it should not be caused by player 1's turn.
    "(sticks > 0 && sticks' = 0) -> !(player_turn = 1)"
}

# Create the specification
specs = spec.GRSpec(env_vars, sys_vars, env_init, sys_init,
                    env_safe, sys_safe)
specs.qinit = '\A \E'
specs.moore = False
specs.plus_one = False

# Synthesize the built in TuLiP way.
print(synth.is_realizable(specs))
ctrl = synth.synthesize(specs)
ctrl._transition_dot_label_format['separator'] = r'\n'
assert ctrl is not None, 'unrealizable'

# Save the controller as a picture. The initial transitions will cover more
# than specified.
if not ctrl.save('two_bits.pdf'):
    print(ctrl)

The code that does work:

from tulip import spec
from tulip import synth

sticks = 7
max_moves = 3

# Specifications
# Environment variables and assumptions
# Formulae governing the model of player 2

env_vars = {
    'player_2_picks': (0, max_moves),
}

env_init = {
    'player_2_picks = 0',
}

env_safe = {
    # If there are remaining sticks and it is player 2's turn
    # (s)he has to pick at least one stick.
    '(sticks > 0 && player_turn = 1) -> (player_2_picks = 1 || player_2_picks = 2 || player_2_picks = 3)',

    # If there is no sticks left, or not player 2's turn
    # player 2 should not be picking any sticks.
    '(sticks = 0 || player_turn != 1) -> player_2_picks = 0',

    # Noone can pick more sticks than what is left.
    'player_2_picks <= sticks',
}

# System variables and guarantees
# Formulae governing the model of player 1, and picking sticks from the stack

sys_vars = {
    'player_1_picks': (0, max_moves),
    'player_turn': (0, 1),
    'sticks': (0, sticks),
}

sys_init = {
    'player_1_picks = 1 || player_1_picks = 2 || player_1_picks = 3',
    'player_turn = 0',
    'sticks = {sticks}'.format(sticks=sticks),
}

sys_safe = {
    # Model of player 1:

    # Same as for player 2
    "(sticks > 0 && player_turn = 0) -> (player_1_picks = 1 || player_1_picks = 2 || player_1_picks = 3)",

    # Same as for player 2
    "(sticks=0 || player_turn != 0) -> player_1_picks = 0",

    # Same as for player 2
    "player_1_picks <= sticks",

    # Model of the game:

    # If it is player 1's turn to pick, subtract her/his choice of
    # number of sticks from the stack.
    "player_turn = 0 -> sticks' = sticks-player_1_picks",

    # Same as previous, but for player 2.
    "player_turn = 1 -> sticks' = sticks-player_2_picks",

    # The turn is alternating while the game goes on (there are sticks left).
    "sticks > 0 -> (player_turn' != player_turn)",

    # Winning strategies for player 1:
    # (Choose one of the three)

    # Player 1 shall never pick all remaining sticks.
    # "(sticks > 0 && player_turn = 0) -> player_1_picks < sticks"

    # If the sticks are depleted during the next step,
    # then it should be caused by player 2's turn.
    # "(sticks > 0 && sticks' = 0) -> player_turn = 1"

    # If the sticks are depleted during the next step,
    # then it should not be caused by player 1's turn.
    "(sticks > 0 && sticks' = 0) -> !(player_turn = 0)"
}

# Create the specification
specs = spec.GRSpec(env_vars, sys_vars, env_init, sys_init,
                    env_safe, sys_safe)
specs.qinit = '\A \E'
specs.moore = False
specs.plus_one = False

# Synthesize the built in TuLiP way.
print(synth.is_realizable(specs))
ctrl = synth.synthesize(specs)
ctrl._transition_dot_label_format['separator'] = r'\n'
assert ctrl is not None, 'unrealizable'

# Save the controller as a picture. The initial transitions will cover more
# than specified.
if not ctrl.save('one_bit.pdf'):
    print(ctrl)

[johnyf]

Summary

I could reproduce the error. A strategy for the first specification is synthesized by tulip.interfaces.omega, and the error is raised when converting the synthesized strategy to a Mealy machine. The strategy appears to be correct for the given first specification, as described below. The results are with ce54897.

The error is raised because the specification formulas allow system transitions outside the range of values that is defined in the variable declaration (and type-checked by tulip.transys.mathset.TypedDict). For variables that take positive values, this can occur for a specification where the variable declaration does not define a range of the form 0..(2^n - 1) (for some value of n).

Automatically generating specification formulas according to variable declarations to avoid this would be implicit. Explicit is better than implicit [PEP 20]. A solution is to include suitable constraints in the specification formulas, as described below.

Observations about the first specification

In the first specification, the system's safety includes the constraint "player_turn = 1 || player_turn = 1". It appears that "player_turn = 1 || player_turn = 2" may be intended.

The first specification allows the system to transition to player_turn' \notin {1, 2}, which allows winning by setting player_turn' = 0 to violate the environment safety constraint (the synthesized strategy is described below).

Specification modifications

Keeping the variable declaration 'player_turn': (1, 2), in the first specification and changing the system safety constraint "player_turn = 1 || player_turn = 1" to

"player_turn = 1 || player_turn = 2",
"player_turn' = 1 || player_turn' = 2",

ensures that the system maintains the invariant player_turn \in {1, 2}.
The synthesized strategy by the function tulip.synth.synthesize in this case is the following.

Strategy synthesized for the first specification

A strategy is synthesized by the interface tulip.interfaces.omega for the first specification ('player_turn': (1, 2) and system safety with "player_turn = 1 || player_turn = 1"), and appears to realize the specification.
The strategy graph is shown below. The system wins in a finite number of steps by either:

• The environment transitioning to player_2_picks = 0 and the system reacting (the game is Mealy) by transitioning to player_turn = 2. In the next time step, this violates the environment safety conjunct '(sticks > 0 && player_turn = 2) -> (player_2_picks = 1 || player_2_picks = 2 || player_2_picks = 3)', so the system wins in a finite number of steps.

• The environment transitioning to player_2_picks \in {1, 2, 3} and the system reacting by transitioning to player_turn = 0. In the next time step, this violates the environment safety constraint '(sticks = 0 || player_turn != 2) -> player_2_picks = 0', so the system wins in a finite number of steps.

The transition to player_turn = 0 raises an error when converting the synthesized strategy from a networkx.DiGraph to a tulip.transys.machines.MealyMachine at

tulip-control/tulip/synth.py

Line 1290 in ce54897

mach.transitions.add(u, v, attr_dict=None, check=False, **d)

The reason for the error is that the Mealy machine attributes are type-checked using the variable declaration. The variable declaration describes the range 'player_turn': (1, 2) but this range is not specified in the specification formulas. As a result, the synthesized strategy includes states where variable player_turn is outside the range 1..2.

Whenever a variable range is not of the form 0..(2^n - 1) (for positive values, and a similar observation holds for negative values too), a symbolic (BDD) representation with a larger range is created by the GR(1) solver in omega.games.gr1.

Automatically generating formulas from the variable declaration 'player_turn': (1, 2) to specify that the variable remain in the range 1..2 would be implicit, so these constraints need to be explicitly included in the system safety specification (as described above for the modified specification).

(The type checking using the class tulip.transys.mathset.TypedDict for edge attributes of the class tulip.transys.labeled_graphs.LabeledDiGraph turns the variable declaration into a constraint for the Mealy machine, whereas for the GR(1) synthesizer omega.games.gr1, the variable declaration is only a type hint, in that it guides the selection of bits for representing the variable values.)

The strategy graph can be obtained by the following change to the module tulip.interfaces.omega.

diff --git a/tulip/interfaces/omega.py b/tulip/interfaces/omega.py
index a4fe595..8a97d35 100644
--- a/tulip/interfaces/omega.py
+++ b/tulip/interfaces/omega.py
@@ -22,6 +22,7 @@ try:
     from omega.games import gr1
     from omega.symbolic import temporal as trl
     from omega.games import enumeration as enum
+    from omega.symbolic import enumeration as sym_enum
 except ImportError:
     omega = None
 import networkx as nx
@@ -60,6 +61,7 @@ def synthesize_enumerated_streett(spec):
     gr1.make_streett_transducer(z, yij, xijk, aut)
     t2 = time.time()
     g = enum.action_to_steps(aut, 'env', 'impl', qinit=aut.qinit)
+    dump_graph_as_figure(g)
     h = _strategy_to_state_annotated(g, aut)
     del z, yij, xijk
     t3 = time.time()
@@ -73,6 +75,13 @@ def synthesize_enumerated_streett(spec):
     return h


+def dump_graph_as_figure(g):
+    """Create a PDF file showing the graph `g`."""
+    h, _ = sym_enum._format_nx(g)
+    pd = nx.drawing.nx_pydot.to_pydot(h)
+    pd.write_png('game_states.png')
+
+
 def is_circular(spec):
     """Return `True` if trivial winning set non-empty.

Details about edge attribute type checking for tulip.transys.machines.MealyMachine

The types for edges of the class tulip.transys.machines.MealyMachine are defined as follows.
The function tulip.synth.strategy2mealy calls the method tulip.transys.machines.MealyMachine.add_inputs.

tulip-control/tulip/synth.py

Lines 1268 to 1269 in ce54897

	inputs = transys.machines.create_machine_ports(env_vars)
	mach.add_inputs(inputs)

The function tulip.transys.machines.create_machine_ports sets the port 'player_turn' domain according to the variable declaration 'player_turn': (1, 2).

tulip-control/tulip/transys/machines.py

Line 78 in ce54897

domain = set(range(start, end + 1))

The method tulip.transys.machines.Transducer.add_inputs sets the attribute _transition_label_def['player_turn'].

tulip-control/tulip/transys/machines.py

Line 259 in ce54897

self._transition_label_def[port_name] = port_type

The method tulip.transys.labeled_graphs.LabeledDiGraph.__init__ sets the attribute self._edge_label_types = self._transition_label_def.

tulip-control/tulip/transys/labeled_graphs.py

Line 793 in ce54897

self._edge_label_types = self._transition_label_def

The method tulip.transys.labeled_graphs.LabeledDiGraph.add_edge creates an instance of tulip.transys.mathset.TypedDict.

tulip-control/tulip/transys/labeled_graphs.py

Lines 970 to 974 in ce54897

	typed_attr = TypedDict()
	typed_attr.set_types(self._edge_label_types)
	typed_attr.update(copy.deepcopy(self._edge_label_defaults))
	# type checking happens here
	typed_attr.update(attr_dict)

The method add_edge then calls the method TypedDict.set_types with argument self._edge_label_types, which equals self._transition_label_def, which includes the range (1, 2) for the port 'player_turn'.

tulip-control/tulip/transys/mathset.py

Lines 796 to 809 in ce54897

	def set_types(self, allowed_values):
	"""Restrict values the key can be paired with.
	@param allowed_values: dict of the form::
	{key : values}
	C{values} must implement C{__contains__}
	to enable checking validity of values.
	If C{values} is C{None},
	then any value is allowed.
	"""
	self.allowed_values = allowed_values

the method add_edge then calls the method TypedDict.update with argument attr_dict. The attr_dict from the strategy includes the value 0 for the variable 'player_turn', and raises an error when type checked.

tulip-control/tulip/transys/mathset.py

Lines 780 to 787 in ce54897

	def update(self, *args, **kwargs):
	if args:
	if len(args) > 1:
	raise TypeError("update expected at most 1 arguments, "
	"got %d" % len(args))
	other = dict(args[0])
	for key in other:
	self[key] = other[key]

tulip-control/tulip/transys/mathset.py

Lines 755 to 774 in ce54897

	def __setitem__(self, i, y):
	"""Raise ValueError if value y not allowed for key i."""
	valid_y = True
	if hasattr(self, 'allowed_values') and i in self.allowed_values:
	valid_y = False
	if self.allowed_values[i] is None:
	valid_y = True
	else:
	try:
	if y in self.allowed_values[i]:
	valid_y = True
	except:
	valid_y = False
	if not valid_y:
	msg = (
	'key: ' + str(i) + ', cannot be'
	' assigned value: ' + str(y) + '\n'
	'Admissible values are:\n\t'
	+ str(self.allowed_values[i]))
	raise ValueError(msg)

The method LabeledDiGraphs.add_edge is called from the method tulip.transys.labeled_graphs.Transitions.add

tulip-control/tulip/transys/labeled_graphs.py

Lines 436 to 443 in ce54897

	def add(self, from_state, to_state, attr_dict=None, check=True, **attr):
	"""Wrapper of L{LabeledDiGraph.add_edge},
	which wraps C{networkx.MultiDiGraph.add_edge}.
	"""
	# self._breaks_determinism(from_state, labels)
	self.graph.add_edge(from_state, to_state,
	attr_dict=attr_dict, check=check, **attr)

The method Transitions.add is called by the function tulip.synth.strategy2mealy above.

Strategy synthesized for "player_turn": (0,3)

For the modified specification with "player_turn": (0,3) a strategy is synthesized and successfully converted to a Mealy machine. The strategy wins the game in a finite number of steps in this case. The removal of deadends would remove all nodes from the Mealy machine, so it is necessary to pass rm_deadends=False to the function tulip.synth.synthesize:

ctrl = synth.synthesize(specs, rm_deadends=False)

The strategy is the following (as a Mealy machine), and is the same with the strategy that is synthesized for the first specification (described above) by tulip.interfaces.omega that raises the error when converted to a Mealy machine.

omega message that dd.cudd is not installed

The message

`omega.symbolic.symbolic` failed to import `dd.cudd`.
Will use `dd.autoref`.

means that the Python implementation of BDDs in dd.autoref and dd.bdd is used, instead of the Cython module dd.cudd that interfaces to the C library CUDD.

This is not expected to affect the synthesis results for this example. The results would be the same when using dd.cudd.

Installing dd.cudd is possible with

pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*
python setup.py install --fetch --cudd

as described in the README of the package dd.

[krooken]

Thank you for your very swift and detailed response.

I tried to find a workaround by constraining the variable in the system safety specification, but I did not realize that I needed the primed variable as well. Thank you for pointing that out. It helps a lot.

I would argue that I have explicitly constrained the variable domain to (1, 2), and the implicit part is encapsulated and happening far away in omega.logic.bitvector. To me, it seems a bit confusing that I need to know the details of the implementation to be able to specify variables' domains correctly. A more pedagogical user interface (with the current way to create bitvectors) would not let me specify a range, but the number of bits needed for a variable instead.

It seems like I run into the same problem also when trying to do synthesis with finite state abstractions. I use tulip.abstract.discretize() and then synthesize tries to assign out of bounds values to loc. I can of course add a constraint to loc in the safety specification, but in this case I find it even more strange that I need to add constraints to a variable that is used completely under the hood of TuLiP.

import tulip as tlp
import tulip.hybrid
import tulip.abstract
import tulip.spec
import tulip.synth
import polytope as poly
import numpy as np

# Continuous state space
cont_state_space = poly.box2poly([[0., 100.], [0., 20.]])

# System dynamics (continuous state, discrete time): simple integrator
h = 1.0
A = np.array([[1.0, h], [0., 1.0]])
B = np.array([[h**2/2.0], [h]])
E = None

# Available control, possible disturbances
U = poly.box2poly(np.array([[-5., 5.]]))
W = None

# Construct the LTI system describing the dynamics
sys_dyn = tlp.hybrid.LtiSysDyn(A, B, E, None, U, W, cont_state_space)

print(sys_dyn)


# Define atomic propositions for relevant regions of state space
cont_props = dict()
cont_props['target'] = poly.box2poly([[99., 100.], [0., 1.]])
cont_props['init'] = poly.box2poly([[0., 1.], [0., 20.]])

# Compute the proposition preserving partition of the continuous state space
cont_partition = tlp.abstract.prop2part(cont_state_space, cont_props)
print(cont_partition)


disc_dynamics = tlp.abstract.discretize(
    cont_partition, sys_dyn,
    closed_loop=False, conservative=True,
    N=5, min_cell_volume=50, plotit=False
)


# disc_dynamics.plot()
print(disc_dynamics)

env_vars = {}

env_init = {}

env_safe = {}

env_prog = {}

sys_vars = {}

sys_init = {
    'init',
}

sys_safe = {
}

sys_prog = {
    'target',
}

spec = tlp.spec.GRSpec(env_vars=env_vars, sys_vars=sys_vars,
                       env_init=env_init, sys_init=sys_init,
                       env_safety=env_safe, sys_safety=sys_safe,
                       env_prog=env_prog, sys_prog=sys_prog)
spec.qinit = '\E \A'

ctrl = tlp.synth.synthesize(spec, sys=disc_dynamics.ts, ignore_sys_init=True)

[johnyf]

A way to avoid the error without mentioning the internal variable loc is to define the initial states (nodes) of the transition system to be any state (node) of the transition system, as follows

disc_dynamics.ts.states.initial.add_from(disc_dynamics.ts.states)

ctrl = tlp.synth.synthesize(
    spec, sys=disc_dynamics.ts, ignore_sys_init=False)

The resulting specification is unrealizable.

[krooken]

Great! Thank you very much!

Yeah, the unrealizability of the last example is the next problem. But that is definitely not caused by TuLiP :) I think I have some hours of work ahead of me :D

[necozay]

I've recently experienced the same problem so maybe keeping this open is better. I would also expect that defining the range of a variable should be enough in order to constrain the valuations of these variables during synthesis.