Check for reachable states which don't hold for the invariant before starting any translation

[jrbeaumont]

At the moment, we check for reachable states in FSM.Translation, because we need to start the translation process to generate the states which we then search. We then use this information to see if any of the reachable states do not hold for the invariant.

I suggest we provide some way of validating the reachable states before we enter FSM.Translation, or STG.Translation for that matter, preferably in Plato.Translation, as part of the validate function, as this will unify all the validation and error reporting.

[jrbeaumont]

I have attempted to implement this (in the reach branch of my repo). Preliminary testing proves it to work, but I aim to do some more tests and then display the results here, for discussion before sending any PRs.

[jrbeaumont]

OK, here is some testing!

Test 1: Standard ME vs Never.

circuit a b c = me a b 
                  <> initialise0 [a, b, c] <> inputs [a, b] <> outputs [c]

Mutual exclusion concepts includes fall a ~> rise b <> fall b ~> rise a, and thus, never [rise a, rise b] holds, as b cannot rise without a falling and vice versa. The output of this is:

.model out
.inputs A B
.outputs C
.internal 
.graph
A0 A+
A+ A1
A1 A-
A- A0
B0 B+
B+ B1
B1 B-
B- B0
C0 C+
C+ C1
C1 C-
C- C0
B0 A+
A+ B0
A0 B+
B+ A0
.marking {A0 B0 C0}
# invariant = not (A && B)
.end

NOTE: This is just STG output, FSM output is also successful. This check occurs before any translation!

If we change this to

circuit a b c = never [rise a, rise b] 
                  <> initialise0 [a, b, c] <> inputs [a, b] <> outputs [c]

We now don't include the fall a ~> rise b <> fall b ~> rise a, meaning that it is possible to reach rise a, rise b.

Attempting to translate this gives us:

Error. 
These signals violate the invariant: 
A
B

I think I am correct in assuming that this is correct. More testing incoming.

[jrbeaumont]

Test 2: Adding a third signal to the never.

In this test, we have:

circuit a b c = never [rise a, rise b, rise c] 
                  <> initialise0 [a, b, c] <> inputs [a, b] <> outputs [c]

Which is basically the same as before, and thus should fail, so let's view the output:

Error. 
These signals violate the invariant: 
A
B
C

Yes it does. But if we include concepts for blocking the reach of SOME of these states:

circuit a b c = never [rise a, rise b, rise c]
                  <> fall a ~> rise b <> fall b ~> rise a
                  <> initialise0 [a, b, c] <> inputs [a, b] <> outputs [c]

This encompasses the requirements to stop a and b being high at the same time. Translating this fails:

Error. 
These signals violate the invariant: 
A
B
C

So now let's add everything to block all of these:

circuit a b c = never [rise a, rise b, rise c]
              <> fall a ~> rise b <> fall a ~> rise c
              <> fall b ~> rise a <> fall b ~> rise c
              <> fall c ~> rise a <> fall c ~> rise b
              <> initialise0 [a, b, c] <> inputs [a, b] <> outputs [c]

These are all the causality concepts necessary to block this, and the translation of this:

.inputs A B
.outputs C
.internals 
.state graph
s1 A- s0
s0 A+ s1
s2 B- s0
s0 B+ s2
s4 C- s0
s0 C+ s4
.marking {s0}
# Warning:
# The following state(s) hold for the invariant but are not reachable:
# s3
# s5
# s6
.end

This time FSM translation (it works for STG too). The warnings there represent: rise a, rise b, rise a, rise c and rise b, rise c, as strictly speaking, we haven't declared these as invariant, so they technically hold for the invariant. This may require some work, but ultimately, the currently declared invariant holds (never [rise a, rise b, rise c]).

One more test incoming.

[jrbeaumont]

Test 3: What if one of the never'ed signals can be informed from another signal.

This doesn't make a great amount of sense, but here's my idea. Having the fall x ~> rise y concepts for each signal is fine, but what if one of the signals causes the transition of another signal not represented in the never concept? Can this be used to check if the never state is reachable?

To do this, I add a buffer of c and d, which should allow us to use d:

circuit a b c d = never [rise a, rise b, rise c] <> buffer c d
              <> fall a ~> rise b <> fall a ~> rise c
              <> fall b ~> rise a <> fall b ~> rise c
              <> fall d ~> rise a <> fall d ~> rise b
              <> initialise0 [a, b, c, d] <> inputs [a, b, d] <> outputs [c]

So we have included buffer c d, but notice the fall d ~> rise a <> fall d ~> rise b concepts. In this case, if d has fallen, then this indicates that c has also fallen, and vice versa. Thus, we should be able to use this here, and our checks for a reachable never state should still pass. We still need to use fall a/fall b ~> rise c as allowing d to rise in this way doesn't necessarily cause c to rise.

The output from translating this:

.model out
.inputs A B D
.outputs C
.internal 
.graph
A0 A+
A+ A1
A1 A-
A- A0
B0 B+
B+ B1
B1 B-
B- B0
C0 C+
C+ C1
C1 C-
C- C0
D0 D+
D+ D1
D1 D-
D- D0
B0 A+
A+ B0
D0 A+
A+ D0
A0 B+
B+ A0
D0 B+
B+ D0
A0 C+
C+ A0
B0 C+
C+ B0
C0 D-
D- C0
C1 D+
D+ C1
.marking {A0 B0 C0 D0}
# invariant = not (A && B && C)
.end

Apologies that this is long, but ultimately, it shows that it translates.

Now let's just double check this by being overly silly. In this case, there will be three gates, buffer c d <> buffer d x <> inverter x y and we replace all the fall d ~> rise ... with rise y ~> rise .... Throwing an inverter into the mix is just to make sure that it's not exclusive to a specific order of signal transitions. Let's try all this:

circuit a b c d x y = never [rise a, rise b, rise c] <> buffer c d <> buffer d x <> inverter x y
              <> fall a ~> rise b <> fall a ~> rise c
              <> fall b ~> rise a <> fall b ~> rise c
              <> rise y ~> rise a <> rise y ~> rise b
              <> initialise0 [a, b, c, d, x, y] <> inputs [a, b, d, x, y] <> outputs [c]

The translation of this:

.model out
.inputs A B D E F
.outputs C
.internal 
.graph
A0 A+
A+ A1
A1 A-
A- A0
B0 B+
B+ B1
B1 B-
B- B0
C0 C+
C+ C1
C1 C-
C- C0
D0 D+
D+ D1
D1 D-
D- D0
E0 E+
E+ E1
E1 E-
E- E0
F0 F+
F+ F1
F1 F-
F- F0
B0 A+
A+ B0
F1 A+
A+ F1
A0 B+
B+ A0
F1 B+
B+ F1
A0 C+
C+ A0
B0 C+
C+ B0
C0 D-
D- C0
C1 D+
D+ C1
D0 E-
E- D0
D1 E+
E+ D1
E1 F-
F- E1
E0 F+
F+ E0
.marking {A0 B0 C0 D0 E0 F0}
# invariant = not (A && B && C)
.end

I believe this works, but these are some fairly simple examples. If it helps I can send a PR so you can see what's going on.

[snowleopard]

A summary of an offline discussion:

I think we should not do state exploration when doing the STG conversion, passing this task to powerful plugins in Workcraft, such as MPSAT.

For the FSM case, let's reuse the state exploration that is already implemented as part of the translation algorithm. This could problably involve refactoring the order of validation and translation steps in the FSM case.

[jrbeaumont]

This was implemented in #71 so I am closing it.