N-ary xor.

Contrast with pure mutual exclusion.

Represent finite domain in GR(1).

An integer or string variable can be used, or multiple Boolean variables.

If the possible values are:

• mutually exclusive (use_mutex == True)
• bool actions have not been requested (bool_actions == False)

then an integer or string variable represents the variable in GR(1).

If all values are integers, then an integer is used. If all values are strings, then a string variable is used. Otherwise an exception is raised, unless Booleans have been requested.

If the values are not mutually exclusive, then only Boolean variables can represent them.

Suppose N possible values are defined. The int variable is allowed to take N+1 values. The additional value corresponds to all, e.g., actions, being False.

If FTS values are integers, then the additional action is an int value.

If FTS values are strings (e.g., 'park', 'wait'), then the additional action is 'none'. They are treated by spec as an arbitrary finite domain.

An option min_one is internally available, in order to allow only N values of the variable. This requires that the variable takes at least one value each time.

Combined with a mutex constraint, it yields an n-ary xor constraint.

Parameters:

• states (iterable container of int or iterable container of str) - values of domain.
• variables - to be augmented with integer or string variable or Boolean variables.
• statevar (str) - name to use for integer or string valued variable.
• bool_states - if True, then use bool variables. Otherwise use integer or string valued variable.

Returns: dict, list

tuple of:

• mapping from values to GR(1) actions. If Booleans are used, then GR(1) are the same. Otherwise, they map to e.g. 'act = "wait"' or 'act = 3'
• constraints to be added to trans and/or init in GR(1)

Convert transition system to GR(1) fragment of LTL.

The attribute FTS.owner defines who controls the system, as described next. It can take values 'env' or 'sys'.

The following are represented by variables controlled by ofts.owner:

• the current state
• the atomic propositions annotating states
• the system actions annotating edges

The following are represented by variables controlled by the other player:

• the environment actions annotating edges

Multiple types of environment and system actions can be defined. Make sure that, depending on the player, 'env' or 'sys' are part of the action type names, so that synth.synthesize can recognize them.

Caution

There are aspects of FTS that need to be separately specified in a logic formula.

An example are the initial conditions constraining the values of environment and system actions.

See also

sys_trans_from_ts, env_open_fts2spec, create_actions, create_states

Parameters:

• ofts - FTS
• ignore_initial (bool) - Do not include initial state info from TS. Enable this to mask absence of FTS initial states. Useful when initial states are specified in another way, e.g., directly augmenting the spec part.
• state_var (str) - name to be used for the integer or string variable that equals the current transition system state.
• bool_states (bool) - deprecated as inefficient

  if True, then use one Boolean variable to represent each state in GR(1). Otherwise use a single integer variable, different values of which correspond to states of ofts.

• bool_actions - Similar to bool_states. For each type of system actions, and each type of environment actions:
  • if True, then for each possible value of that action type, use a different Boolean variable to represent it.
  • Otherwise use a single integer variable, that ranges over the possible action values.

Returns: GRSpec

logic formula in GR(1) form representing ofts.

Convert env transition system to GR(1) representation.

The following are represented by environment variables:

• the current state
• the atomic propositions annotating states
• the environment actions annotating edges

The following are represented by system variables:

• the system actions annotating edges

Multiple types of environment and system actions can be defined.

For more details see sys_to_spec.

See also

sys_open_fts2spec

Return a dict of substitution rules for dependent variables.

The dependent variables in a transition system are the atomic propositions that are used to label states.

They are "dependent" because their values are completely determined by knowledge of the current state in the transition system.

The returned substitutions can be used

Parameters:

• statevar - name of variable used for the current state For example if it is 'loc', then the states 's0', 's1' are mapped to:

   {'s0': '(loc = "s0")',
    's1': '(loc = "s1")'}
  

• state_ids (dict)
• fts (FTS)

Returns: {'p': '((loc = "s1") | (loc = "s2") | ...)', ...} where:

• 'p' is a proposition in fts.atomic_propositions
• the states "s1", "s2" are labeled with 'p'
• loc is the string variable used for the state of fts.

For each proposition find the states labeled with it.

Parameters:

• fts (FTS)

Returns: {'p': s, ...} where 'p' a proposition and s a set of states in fts.

Synthesize from logic specs and multiple transition systems.

The transition systems are composed synchronously, i.e., they all have to take a transition at each time step. The synchronous composition is obtained by taking the conjunction of the formulas describing each transition system.

The states of each transition system can be either:

• all integers, or
• all strings

In either case the transition system state will be represented in logic with a single variable, that ranges over a finite set of integers or strings, respectively.

The keys of ts are used to name each state variable. So the logic formula for ts['name'] will be 'name'.

Who controls this state variable is determined from the attribute FTS.owner that can take the values:

• 'env'
• 'sys'

For example:

>>> ts.states.add_from(xrange(4))
>>> ts['door'].owner = 'env'

will result in a logic formula with an integer variable 'door' controlled by the environment and taking values over {0, 1, 2, 3}.

The example:

>>> ts.states.add_from(['a', 'b', 'c'])
>>> ts['door'].owner = 'sys'

will instead result in a string variable 'door' controlled by the system and taking values over {'a', 'b', 'c'}.

Parameters:

• solver (str) - 'gr1c' or 'slugs' or 'jtlv'
• ignore_init (set of keys from ts)
• bool_actions (set of keys from ts)
• specs (GRSpec)
• ts (dict of FiniteTransitionSystem)

Function to call the appropriate synthesis tool on the specification.

There are three attributes of C{specs} that define what
kind of controller you are looking for:

1. C{moore}: What information the controller knows when deciding the next
   values of controlled variables:
    - Moore: can read current state,
      but not next environment variable values, or
    - Mealy: can read current state and next environment variable values.

2. C{qinit}: Quantification of initial variable values:
    Whether all states that satisfy a predicate should be winning,
    or the initial values of some (or all) the variables is
    subject to the synthesizer's choice.

3. C{plus_one}: The form of assume-guarantee specification,
    i.e., how the system guarantees relate to assumptions about the
    environment.

For more details about these attributes, see L{GRSpec}.

The states of the transition system can be either:

  - all integers, or
  - all strings

For more details of how the transition system is represented in
logic look at L{synthesize_many}.

Beware!
=======
This function provides a generic interface to a variety
of routines.  Being under active development, the types of
arguments supported and types of objects returned may change
without notice.

@param option: Magic string that declares what tool to invoke,
    what method to use, etc.  Currently recognized forms:

    For GR(1) synthesis:

      - C{"gr1c"}: use gr1c via L{interfaces.gr1c}.
        written in C using CUDD, symbolic

      - C{"gr1py"}: use gr1py via L{interfaces.gr1py}.
        Python, enumerative

      - C{"omega"}: use omega via L{interfaces.omega}.
        Python using C{dd} or Cython using CUDD, symbolic

      - C{"slugs"}: use slugs via L{interfaces.slugs}.
        C++ using CUDD, symbolic

      - C{"jtlv"}: use JTLV via L{interfaces.jtlv}.
        Java, symbolic
        (deprecated)

@type specs: L{spec.GRSpec}

@param env: A transition system describing the environment:

        - states controlled by environment
        - input: sys_actions
        - output: env_actions
        - initial states constrain the environment

    This constrains the transitions available to
    the environment, given the outputs from the system.
@type env: L{FTS}

@param sys: A transition system describing the system:

        - states controlled by the system
        - input: env_actions
        - output: sys_actions
        - initial states constrain the system

@type sys: L{FTS}

@param ignore_env_init: Ignore any initial state information
    contained in env.
@type ignore_env_init: bool

@param ignore_sys_init: Ignore any initial state information
    contained in sys.
@type ignore_sys_init: bool

@param rm_deadends: return a strategy that contains no terminal states.
@type rm_deadends: bool

@return: If spec is realizable,
    then return a Mealy machine implementing the strategy.
    Otherwise return None.
@rtype: L{MealyMachine} or None

Check realizability.

For details see synthesize.

Convert strategy to Mealy transducer.

Note that the strategy is a deterministic game graph, but the input A is given as the contraction of this game graph.

Parameters:

• A (networkx.DiGraph) - strategy
• spec (GRSpec)

Returns: MealyMachine

Return a determinized copy of mach with given initial outputs.

The transducers produced by synthesis can have multiple initial output valuations as possible reactions to a given input valuation.

Possible reasons for this are:

1. the system does not have full control over its initial state. For example the option "ALL_INIT" of gr1c.
2. the strategy returned by the solver has multiple vertices that satisfy the initial conditions.

Case 1

Requires an initial condition to be specified for each run of the transducer, because the transducer does not have full freedom to pick the initial output values.

Note that solver options like "ALL_INIT" assume that the system has no control initially. Any output valuation that satisfies the initial conditions can occur.

However, this may be too restrictive. The system may have control over the initial values of some outputs, but not others.

For the outputs it can initially control, the non-determinism resulting from synthesis is redundancy and can be removed arbitrarily, as in Case 2.

Case 2

The function strategy2mealy returns a transducer that for each initial input valuation, for each initial output valuation, reacts with a unique transition.

But this can yield multile reactions to a single input, even for solver options like "ALL_ENV_EXIST_SYS_INIT" for gr1c. The reason is that there can be multiple strategy vertices that satisfy the initial conditions, but the solver included them not because they are needed as initial reactions, but to be visited later by the strategy.

These redundant initial reactions can be removed, and because the system has full control over their values, they can be removed in an arbitrary manner, keeping only a single reaction, for each input valuation.

Algorithm

Returns a deterministic transducer. This means that at each transducer vertex, for each input valuation, there is only a single reaction (output valuation) available.

The non-determinism is resolved for the initial reaction by ensuring the outputs given in init_out_values take those values. The remaining outputs are determinized arbitrarily.

See also

synthesize, strategy2mealy

Parameters:

• mach (MealyMachine) - possibly non-deterministic transducer, as produced, for example, by synthesize.
• init_out_values (dict) - mapping from output ports that the system cannot control initially, to the initial values they take in this instance of the game.

Returns: MealyMachine