ftsrg / gamma

An Eclipse-based modeling framework for the component-based design and analysis of reactive systems
http://gamma.inf.mit.bme.hu
30 stars 25 forks source link

Promela fixes #152

Closed Rorck closed 1 year ago

Rorck commented 1 year ago

Added acceptance cycle as result.

Modified trivial branch serialization: previous version caused unwanted acceptance cycles because of the true guard:

:: true -> atomic {
    «action.serialize»
}

now the guard has to be evaluated at every step, causing valid acceptance cycle counter-examples:

:: «action.serialize» -> atomic {
    skip
}