# Import the packages that we need
from __future__ import print_function

import logging

from tulip import transys, spec, synth
from tulip.transys import machines

"""
Explanation: Discrete Transition System Example
Richard Murray, 30 Jul 2013
This example illustrates the use of TuLiP to synthesize a reactive
controller for system whose dynamics are described by a discrete
transition system.
End of explanation
"""


# Create a finite transition system
sys = transys.FTS()

# Define the states of the system
sys.states.add_from(['X0', 'X1', 'X2', 'X3', 'X4', 'X5'])
sys.states.initial.add('X0')    # start in state X0

# Define the allowable transitions
sys.transitions.add_comb({'X0'}, {'X1', 'X3'})
sys.transitions.add_comb({'X1'}, {'X0', 'X4', 'X2'})
sys.transitions.add_comb({'X2'}, {'X1', 'X5'})
sys.transitions.add_comb({'X3'}, {'X0', 'X4'})
sys.transitions.add_comb({'X4'}, {'X3', 'X1', 'X5'})
sys.transitions.add_comb({'X5'}, {'X4', 'X2'})

# Add atomic propositions to the states
sys.atomic_propositions.add_from({'home', 'lot'})
sys.states.add('X0', ap={'home'})
sys.states.add('X5', ap={'lot'})

"""
Explanation: System dynamics
The system is modeled as a discrete transition system in which the
robot can be located anyplace on a 2x3 grid of cells.  Transitions
between adjacent cells are allowed, which we model as a transition
system in this example (it would also be possible to do this via a
formula)
We label the states using the following picture
+----+----+----+
| X3 | X4 | X5 |
+----+----+----+
| X0 | X1 | X2 |
+----+----+----+
End of explanation
"""


env_vars = {'park'}
env_init = set()                # empty set
env_prog = '!park'
env_safe = set()                # empty set

"""
Explanation: Environment variables and specification
The environment can issue a park signal that the robot must respond
to by moving to the lower left corner of the grid.  We assume that
the park signal is turned off infinitely often.
End of explanation
"""


# Augment the system description to make it GR(1)
sys_vars = {'X0reach'}          # infer the rest from TS
sys_init = {'X0reach'}
sys_prog = {'home'}             # []<>home
sys_safe = {'(X (X0reach) <-> lot) || (X0reach && !park)'}
sys_prog |= {'X0reach'}

# Create the specification
specs = spec.GRSpec(env_vars, sys_vars, env_init, sys_init,
                    env_safe, sys_safe, env_prog, sys_prog)

"""
Explanation: System specification
The system specification is that the robot should repeatedly revisit
the upper right corner of the grid while at the same time responding
to the park signal by visiting the lower left corner.  The LTL
specification is given by
[]&lt;&gt; home &amp;&amp; [](park -&gt; &lt;&gt;lot)

Since this specification is not in GR(1) form, we introduce the
variable X0reach that is initialized to True and the specification
[](park -&gt; &lt;&gt;lot)

becomes
[](X (X0reach) &lt;-&gt; lot || (X0reach &amp;&amp; !park))
End of explanation
"""


# Moore machines
# controller reads `env_vars, sys_vars`, but not next `env_vars` values
specs.moore = True

# synthesizer should find initial system values that satisfy
# `env_init /\ sys_init` and work, for every environment variable
# initial values that satisfy `env_init`.
specs.qinit = '\E \A'
ctrl = synth.synthesize(specs, sys=sys)

# Make sure the specification was realizable
assert ctrl is not None, 'unrealizable'

# Print out the strategy
print(ctrl)

# Simulate the strategy
machines.random_run(ctrl, N=10)

"""
Explanation: Controller synthesis
At this point we can synthesize the controller using one of the available
methods.
End of explanation
"""


