You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
type Message is
message
F1 : F1
then F2
if <condition>,
then F3
if <other condition>;
F2 : F2
then FCS;
F3 : F3;
FCS : FCS;
end message;
The prev_field function is not able to correctly return the predecessor of FCS, because it only checks, whether the condition of an incoming edge can be evaluated to true. It than assumes that the source field of the edge is the predecessor of the given field. As edges form F2 and F3 to FCS both have the condition true, the field which is evaluated first is assumed to be the predecessor of FCS (but not necessarily the right one). The same applies for the _get_length_unchecked function.
To solve this, i would introduce a check, if the assumed predecessor field has been set.
The text was updated successfully, but these errors were encountered:
Suppose the following Spec:
The
prev_field
function is not able to correctly return the predecessor of FCS, because it only checks, whether the condition of an incoming edge can be evaluated to true. It than assumes that the source field of the edge is the predecessor of the given field. As edges form F2 and F3 to FCS both have the conditiontrue
, the field which is evaluated first is assumed to be the predecessor of FCS (but not necessarily the right one). The same applies for the_get_length_unchecked
function.To solve this, i would introduce a check, if the assumed predecessor field has been set.
The text was updated successfully, but these errors were encountered: