"single action" test is failing (SMCDEL.Translations)

[m4lvin]

The "single action" test defined here sometimes fails. See for example https://gitlab.com/m4lvin/SMCDEL/-/jobs/625710207#L377.

The relevant S5 action model and formula:

ActMS5
  [(0,(Top,[]))
  ,(1,(Xor [Neg Top],[]))
  ,(2,(Xor [Bot],[(P 2,PrpF (P 0))]))
  ,(3,(Bot,[]))
  ]
  [("0",[[0],[1],[2],[3]])
  ,("1",[[0,1,2,3]])
  ,("2",[[0,1,2,3]])
  ,("3",[[0,1,2,3]])
  ,("4",[[0,1,2,3]])
  ,("5",[[0,1,2,3]])
  ]

Kw "1" (PrpF (P 2))

[m4lvin]

Another failing input:

ActMS5
  [ (0,(Top,[]))
  , (1,(Bot,[]))
  , (2,(Bot,[(P 3,PrpF (P 1))]))
  , (3,(Neg (Impl (Conj [Top,Bot,Bot]) (Disj [PrpF (P 2),PrpF (P 1)])),[]))
  ]
  [ ("0",[[0],[1],[2],[3]])
  , ("1",[[0,1,2,3]])
  , ("2",[[0,1,2,3]])
  , ("3",[[0,1,2,3]])
  , ("4",[[0,1,2,3]])
  , ("5",[[0,1,2,3]])
  ]

Ck ["1"] (PrpF (P 3))

[m4lvin]

A minimum counter-example, note that this contains factual change making p2 true.

$ stack smcdel:test:translations
λ> let actm = ActMS5 [(0,(Top,[])) ,(1,(Bot,[(P 2,Top)])) ] [("0",[[0],[1]]) ,("1",[[0,1]]) ,("2",[[0,1]]) ,("3",[[0,1]]) ,("4",[[0,1]]) ,("5",[[0,1]]) ] in let f = K "1" (PrpF (P 2)) in singleActionTest actm f
[False,True,True,False]

The underlying problem is that actionToTransformerWithMap and thus actionToEvent (used to give the second and third answer in singleActionTest), when choosing the fresh variables to label the actions only avoid those occurring in the pre- and postconditions, but not the propositions themselves that are changed:

https://github.com/jrclogic/SMCDEL/blob/6e354ddb76d51f8f7b19759466e1c9be2ba094b7/src/SMCDEL/Translations/S5.hs#L167

Hence in this case p2 is considered fresh. The fix will be to also include the changed propositions in this line.

See also this previous attempt to repair the same problem: https://github.com/jrclogic/SMCDEL/commit/53a9ac879865022a2e8c2c426ca59195f97b0cef