symphonytool / symphony

The Symphony IDE
5 stars 4 forks source link

POG: Exists predicate generated for implicit ops with no arguments or state #298

Closed ldcouto closed 9 years ago

ldcouto commented 9 years ago

Minimum example:

process A =  begin
operations
op ()
post true
@Skip
end

This gives a sat PO of the form (exists @ true). That's wrong. If the operation has no parameters, then no quantifier should be introduced.