habtom / factum

Architectural Design Constraints Specification and Verification
GNU General Public License v3.0
1 stars 1 forks source link

act_pb generates forall p instead of forall q #39

Closed dmarmsoler closed 6 years ago

dmarmsoler commented 6 years ago

the variable generated after \\<^sub>c in act_pb must be q, not p. May be wrong in specification

habtom commented 6 years ago

Yes, was specification problem fixed in the model