Added support for invariants

[jrbeaumont]

This includes:

• Support for invariants as a part of CircuitConcept.

• Translating FSMs will no longer insert invariant states.

• Translating STGs will report on what sets of transitions must occur to reach invariant states.

• No translation will occur if the provided initial state is an invariant state.

[snowleopard]

@jrbeaumont I've added a bunch of comments. Let me know when you are ready for another iteration.

[jrbeaumont]

@snowleopard: Here is iteration 2 :)

[snowleopard]

Going in the right direction... :)

[jrbeaumont]

@snowleopard: Are you aware of a way to filter by pattern? I have changed UnusedSignal [a] etc to UnusedSignal a, but I need to map all the signals by their patterns, only if there are those types of errors. Doing filter (==UnusedSignal) errors or anything similer, such as ==(UnusedSignal a) will not work.

[snowleopard]

@jrbeaumont I don't understand, can you give an example?

[jrbeaumont]

So I have a list: [ValidationError a] In this case, let's say it consists of: [UnusedSignal x, UndefinedInitialState x, InvariantInitialState x, InvariantInitialState y] x and y are the erroneous signals.

When it comes to preparing the outputs to inform the users what signals are erroneous, I would like to filter by all the ValidationError a types, so I can have:

[UnusedSignal x] [UndefinedInitialState x] [InvariantInitialState x, InvariantInitialState y]

This will then allow me to add the information on what is wrong with the signals, i.e. "The following signals are not defined is inputs, outputs or internals", and then list the signals, in this case x. Then I can do the same for UndefinedInitialState, in this case x again, InconsistentInitialState will not have any signals so no output will be produced for this, and for InvariantInitialState the output will include x and y.

My issue is, because these are types including arguments (Each type includes a, i.e. UnusedSignal a) I cannot filter the full list of [ValidationError a] to simply provide me with lists for each of these types. How can I filter for each type of ValidationError a

[snowleopard]

@jrbeaumont I see, thanks! I think the following list comprehension trick should work:

unused :: [ValidationError a] -> [a]
unused es = [ a | UnusedSignal a <- es ]

In list comprehensions, if the pattern match fails the current element is skipped.

See https://en.wikibooks.org/wiki/Haskell/Pattern_matching#List_comprehensions.

[jrbeaumont]

That's great, thank you!

[jrbeaumont]

@snowleopard: OK, here is the third iteration :)

[jrbeaumont]

@snowleopard: As the latest commits suggest, only reachable states will be inserted for FSMs.

If any non-invariant states are reachable an error will be produced instead of an FSM. A warning will be given if any states are not reachable, but are not declared as non-invariant. If reachability=inv, then this information is printed.

Please have a look when you get time and let me know!

Edit: Am I explaining this all correctly? I've spent so long staring at the words invariant and non-invariant I've forgotten which is which :|

[snowleopard]

@jrbeaumont I left some comments. Some of the comments are very non-constructive, sorry, but I didn't have time to investigate further :-)

Edit: Am I explaining this all correctly? I've spent so long staring at the words invariant and non-invariant I've forgotten which is which :|

Yes, I think in this version "invariant" is used correctly :)

Although I don't think the word is used as an adjective, so "non-invariant state" feels strange. I'd say "state where the invariant doesn't hold" -- a lot more verbose, but sounds familiar.

[jrbeaumont]

Thank you @snowleopard, I will get to these comments :)

I see what you mean about it not being an adjective, but I'm considering renaming the error type InvariantInitialState to NonInvariantInitialState so it makes more sense, as if the initial state holds the invariant, an error calling it "InvariantInitialState" may be confusing. What do you think?

[snowleopard]

Ah, I missed that. InvariantInitialState is indeed incorrect. But now, since you are reporting an error if the invariant is violated in general (not only in the initial state), why not call it InvariantViolated?

[jrbeaumont]

That's a good idea. However, for the invariants being reachable in FSMs, this is only recognised after the validation. I can create this as this type of error anyway, for clarity, but it will have to be dealt with in the same way as it is in this iteration.

[snowleopard]

However, for the invariants being reachable in FSMs, this is only recognised after the validation

Why? If the invariant is broken, the specification is invalid. So, I don't see why this should be treated differently from other errors.

[jrbeaumont]

This happens because the validation occurs, then if this is valid, the FSM translation starts, where we then find the reachable states, which then throws an error, but we cannot return an invalid from the translate function.

On 1 Mar 2017, at 23:56, Andrey Mokhov notifications@github.com wrote:

However, for the invariants being reachable in FSMs, this is only recognised after the validation

Why? If the invariant is broken, the specification is invalid. So, I don't think why this should be treated differently from other errors.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

[snowleopard]

Well, still it doesn't make sense to verify the initial state separately, if all states are being verified. Just remove this check altogether.

[jrbeaumont]

That's a good idea. I will have a think and see if there is a way to check for reachable states which don't hold for the invariant before we start any translation, so an Invalid is passed into the translate function of either FSM or STG translation files.

[jrbeaumont]

@snowleopard: I have an idea for checking for reachable states which don't hold for the invariant in the validation function, before we try to translate anything. Please let me know what you think:

The idea is, we have all the arcs, consisting of ([causes], effect). If we have a never concept: never [rise a, rise b], we can check the arcs.

Let's take the first transition of this never: rise a. Using this, let's filter all of the arcs where the effect is rise a. Now, if we look at all of the causes for rise a, we can check to see if fall b is one of them, specifically, the opposite of the other transition of the never concept. If we find it, then this means that b must be 0 before rise a can occur.

If this is not found, we then check for fall b in all of the causes for these causes (causes where each cause of rise a is an effect in an arc). If we find fall b then no invariant is found. Otherwise, use repeat this step with all the causes of these, and so on and so forth.

We can keep a list of visited effect transitions, so we don't repeat. If we never find this fall b transition, then then it is possible to reach a state where rise a and rise b have occurred. We can stop early if we find rise b.

I have a feeling I'm missing something with this, but even for lists of causes for OR causality, if any of the possible causes are rise b, it can reach a state that it shouldn't.

We could even sequence the causes before hand, which would provide us with all of the necessary combinations of causes so we know exactly what we're dealing with. In the event there is some OR-causality which only one of the possible causes features fall b this will fail too.

I might give it a try and see if I hit any roadblocks.

[jrbeaumont]

@snowleopard: Thank you for all of these comments. If you have any further, let me know and I will get to them :)

Have you had chance to read my above comment?

[snowleopard]

@jrbeaumont Ah, I missed the above comment. I suggest not to go that way for now. Let's fix minor things and commit this solution, perhaps, creating an issue if you'd like to improve something in a substantial way.

[jrbeaumont]

No problem :)

That's fair. I would like to give it a try, as if we can check that no invariant states in Plato.Translation all errors will be found/reported before we even start to try and translate to an FSM/STG. I will fix any more changes you suggest, and I will make an issue.

[snowleopard]

Merged now!