empty graph returned as explicit strategy for trivially realizable problem

[johnyf]

Setting the assumption False to obtain a trivially realizable GR(1) spec results in an enumerated strategy that does not have any nodes. As of 45102830c21614b669517bfceefd5214662813a5 the spec:

[INPUT]
x
[OUTPUT]
y
[SYS_LIVENESS]
0

is not realizable, as expected. The variation with:

[INPUT]
x
[OUTPUT]
y
[ENV_LIVENESS]
0
[SYS_LIVENESS]
0

is realizable, as expected.

The issue is with the spec:

[ENV_INIT]
0

Irrespective of the values for the other parts (for env and sys), the above spec returns:

RESULT: Specification is realizable.
{"version": 0,
 "slugs": "0.0.1",

 "variables": ["x", "y"],

 "nodes": {
}}

Correctly, it is realizable. But incorrectly for an enumerated strategy representation, the transducer graph has no nodes (it should have been non-empty, since any infinite system behavior is an admissible solution in this case).

It appears that the assumption on initial condition prevents the enumeration of the game graph in extensionExtractExplicitStrategy. Simplified, this line reads:

todoInit = winningPositions & initSys & initEnv

If initSys = False, then todoInit is the empty set, so an empty todoList will result, because there will be 0 iterations. As a result, no nodes will be enumerated later.

Changing that line to (assumption -> guarantee):

( (! initEnv) | (winningPositions & initSys) )

seems to fix the issue, returning for the previous spec:

[ENV_INIT]
0

the enumerated strategy:

{"version": 0,
 "slugs": "0.0.1",

 "variables": ["x", "y"],

 "nodes": {
"0": {
    "rank": 0,
    "state": [0, 0],
    "trans": [0, 2]
},

"1": {
    "rank": 0,
    "state": [0, 1],
    "trans": [0, 2]
},

"2": {
    "rank": 0,
    "state": [1, 0],
    "trans": [0, 2]
},

"3": {
    "rank": 0,
    "state": [1, 1],
    "trans": [0, 2]
}

}}

[johnyf]

Although the suggestion above returns an enumerated strategy even for trivially realizable problems, however the strategy is not very useful. For example, with 16 propositional variables, a graph with all 65536 nodes is returned as strategy!

The previous result of reporting realizability but returning an empty graph as strategy appears to serve better the intention of reporting a case of trivial realizability. However, it is implicit and not evident from the output (that is unexpected).

Considering that trivially realizable (anomalous) problems are undesired in the first place, it is suggested that the solver explicitly report "trivial realizability" if it detects False assumption for the initial condition.

[vraman]

On Thu, Jan 15, 2015 at 7:55 PM, Ioannis Filippidis < notifications@github.com> wrote:

it is suggested that the solver explicitly http://legacy.python.org/dev/peps/pep-0020/ report "trivial realizability" if it detects False assumption for the initial condition.

I would advocate against this, as it opens the door to reporting all sorts of additional information about the synthesized Mealy machine at synthesis time, e.g. whether it encodes a finite strategy, whether the system goals are achieved, etc. Rather, this sort of information is made available by running tools/createSpecificationReport.py.

Vasu

[progirep]

Hi johnyf, thanks for your report.

In explicit strategy extraction, only reachable states are added. If there is an environment initialisation assumption that is effectively "False", then there is no initial state that is reachable by correct environment behavior, and thus, the state set is empty. This is why there is no suitable state. The line

todoInit = winningPositions & initSys & initEnv

is there because we want to fill "todoinit" with reachable initial winning states, so all states must be in winningPositions and safety "initEnv" (as otherwise they would be losing or non-reachable) . However, as we are extracting a strategy for the system, all initial states also have to satisfy "initSys". Thus, we have both "initSys" and "initEnv" as conjuncts in this line.

We could, by the way, add states that do not satisfy the initialization assumptions, as you suggested. We won't necessarily get 65536 states if we have 16 propositions as the system initialization guarantees would also need to be satisfied, so there would typically be fewer. However, in this case one would wonder whether it also makes sense to also add transitions that violate the safety assumptions whenever the output can be set along the transition such that the safety guarantees can still be met. This is the same concept, only for transitions instead of initial states. Again, the explicit-state strategy would seriously blow up. When adding additional "tolerable" transitions, the (originally) requsted behavior is already supported (and called "oneStepRecovery" - accessible as an option to slugs).

I also agree with Vasu's statement. Admittedly, a warning could be issued in this case so that a program reading a strategy could be informed.However, an empty automaton can only be the output of a realizable specification if there is indeed no initial state, so requiring the program processing the strategy to read this warning is actually more difficult than just checking if the size of the strategy is 0.