semantics icon indicating copy to clipboard operation
semantics copied to clipboard

[KISEMA-1589] Strong Self Abort Semantics

Open fabianheyer opened this issue 3 years ago • 0 comments

[Issue KISEMA-1589 migrated from JIRA, first reported on 2020-06-11]

In the given example, for region StrongAbort: Following the idea of sequential constructiveness, the triggers of strong aborts (here: x > 0) should be evaluated - once - sequentially before the body of the aborted state (here: x += 1) is executed. As it is implemented now, the trigger x > 0 is evaluated before x += 1, and then again, after x += 1.

scchart SeqAbort {
  output int x = 0, y = 0, ticks = 0

  region tickCnt {
    
    initial state Cnt ""
    do ticks++ go to Cnt
  }
    
  region StrongAbort {
    initial state S {
      initial state S1
      do x += 1 go to S1
    }
    immediate if x > 0 do x += 10 abort to T

    state T {
      initial state T1
      immediate do x += 100 go to T2
      
      state T2
      go to T1
    }
 }

  region WeakAbort {
    initial state S {
      initial state S1
      do y += 1 go to S1
    }
    immediate if y > 0 do y += 10 go to T

    state T {
      initial state T1
      immediate do y += 100 go to T2
      
      state T2
      go to T1
    }
  }
}

seqAbort-bug

fabianheyer avatar Apr 19 '22 10:04 fabianheyer