eclipse-qvtd-bot
commented
2 weeks ago By Ed Willink on Dec 29, 2019 10:14
PredicateEdge seems to have multiple semantics.
name = null for an operation result e.g 'result' = true.\ name = '=' for an operation result e.g 'result' = true.\ name = 'includes' for acollection membership e.g 'set' includes 'member'
?? always '=' or 'includes' \ ?? implement PredicateEdge.isPartial to distinguish the two semantics
| --- | --- | | Bugzilla Link | 558675 | | Status | NEW | | Importance | P3 normal | | Reported | Dec 29, 2019 05:27 EDT | | Modified | Dec 29, 2019 10:14 EDT | | See also | 552853, 547247 | | Reporter | Ed Willink |
Description
The SeqToStm scheduling fails once a bug in ReachabilityForeest getPrecessors is fixed; PredicateEdge does not define a unique reachability predecessor since <> is an N:1 relationship.
In:
domain seqDgm \ m1:Message \ {\ messageId = mid,\ event = eSet:Set(MessageEvent) {\ send:MessageEvent {type = MessageEventType::Send, state = ist1:State{}},\ receive:MessageEvent {type = MessageEventType::Receive, state = ist2:State{}}\ ++ _\ },\ interaction = i:Interaction{}\ };
we need to evaluate
let send = eSet->select(type = MessageEventType::Send and state = ist1:State{})\ in rest = eSet->excluding(send) in\ let receive = eSet->select(type = MessageEventType::Receive and state = ist2:State{}) in ...
in order to determine the 'unique' values of send and receive from\ eSet derived from the m1 head\ ist1 derived from the when_StateToState head\ ist2 derived from the when_StateToState1 head
This is not really possible since there is no guarantee that there are not zero or two or more matches for the select. zero is ok, the match fails. two is a problem, distinct mapping invocations could have done something distinct for each.
It looks as if the head choices should have been {send, receive, when_StateToState, when_StateToState2} rather than {m1, when_StateToState, when_StateToState2}