saeaadl / aadlv2.2

SAE AADL core language, version 2.2
1 stars 0 forks source link

Deterministic mode transitions #36

Open joeseibel opened 5 years ago

joeseibel commented 5 years ago

Legality rule L3 in section 12 contains the sentence, "For each mode, there must exist exactly one transition, which can cause transition to another mode."

This sentence is trying to explain what a deterministic transition function is, but it ends up being too restrictive. The current wording does not permit branching to different modes based upon different triggers. It also doesn't allow final modes as each mode must have exactly one transition from that mode.

The sentence should be something like, "For each pair of source mode and trigger, there can be at most one transition."

joeseibel commented 5 years ago

Also, the first sentence of L3 is, "The set of transitions declared within a single component implementation must define a deterministic transition function."

"component implementation" should be replaced with "component classifier" in that sentence.

jjhugues commented 3 years ago

Captured in the document (L3) mentions that for each mode, there must exist at most one trigger which cause transitions to another mode

at most : we do not need a live automata, having a terminal mode is fine trigger is what we need, it is equivalent to Joe's formulation