kieler/semantics

[KISEMA-1416] Mixing termination and abort yields unschedulable model with lean approach

fabianheyer opened this issue · 0 comments

[Issue KISEMA-1416 migrated from JIRA, first reported on 2019-08-23]

Consider the following model:

scchart UserInteractionStateMachine {
--
input bool I1, I2  initial state S1 {    initial state S1_1
if I1 go to S1_2    final state S1_2
}
if I2 go to Aborted
join to Terminated  state Aborted
state Terminated
}

AbortTerminationNonLean

If I try to compile this model with the statebased lean approach, the model is unschedulable due to cyclic region dependencies.

AbortTerminationNonLean_Unschedulable

I see the cycle in the model during compilation. However, since the original model doesn't show concurrency, I think it should be possible to schedule it in some lean way.

For the moment I can work around the issue by replacing the termination transition with another weak abort and replicating the original guard from the inner region.