repair S5.actionToEvent: also avoid props in postconditions

jrclogic · Jan 11, 2019 · 53a9ac8 · 53a9ac8
1 parent df71fbb
commit 53a9ac8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/SMCDEL/Translations/S5.hs b/src/SMCDEL/Translations/S5.hs
@@ -132,7 +132,7 @@ actionToEvent (ActMS5 acts actrel, faction) = (KnTrf addprops addlaw changeprops
   actions = map fst acts
   ags          = map fst actrel
   addprops     = actionprops ++ actrelprops
-  (P fstnewp)  = freshp $ propsInForms (map (fst.snd) acts)
+  (P fstnewp)  = freshp . propsInForms $ concat [ pre : map snd posts | (_,(pre,posts)) <- acts] -- avoid props in pre- and postconditions
   actionprops  = [P fstnewp..P maxactprop] -- new props to distinguish all actions
   maxactprop   = fstnewp + ceiling (logBase 2 (fromIntegral $ length actions) :: Float) -1
   actpropsRel  = zip actions (powerset actionprops)