Draft: Code to compute an automaton from clauses.

experiments/contract-automata/src/ContractAutomaton.hs

@@ -35,7 +35,7 @@ For a contract with action alphabet Σ, we will introduce its deontic alphabet 
 
 -- | The state of a contract automaton. It is possible for a CA state to contain 0 clauses.
 newtype CAState = MkCAState { clauses :: [Clause] }
-  deriving newtype (Eq, Ord, Finite)
+  deriving newtype (Eq, Ord, Finite, Semigroup)
   deriving stock Show
 
 contractToCAState :: Contract -> CAState

experiments/contract-automata/src/Eval.hs

@@ -8,6 +8,12 @@ import           Syntax
 -- import Data.Coerce (coerce)
 import           Control.Bool
 import           Control.Monad.Identity    (Identity (..))
+import           Data.Coerce
+import           Data.Containers.ListUtils
+import           Data.Map.Strict           (Map)
+import qualified Data.Map.Strict           as Map
+import qualified Data.Map.Merge.Strict     as Map
+import           Data.List
 
 {----------------------
   Resources / See also
@@ -70,10 +76,135 @@ synchronouslyCompose :: (Clause -> Event -> Clause) -> [Clause] -> Event -> [Cla
 synchronouslyCompose clauseResidual = \clauses event -> fmap (`clauseResidual` event) clauses
   -- synchronous composition corresponds to conjunction over clauses
 
+data Transitions s =
+  MkTransitions (Map Event s) s
+  deriving (Show, Functor)
+
+data Transitions' =
+  MkTransitions' [(Condition, CAState)] CAState
+
+data Condition =
+  MkCondition [PosNeg]
+
+data PosNeg =
+  Pos Event | Neg Event
+
+topState :: CAState
+topState = MkCAState []
+
+bottomState :: CAState
+bottomState = MkCAState [Bottom]
+
+-- MkTransitions (Map.fromList [(e1, cs1), (e2, cs2)]) cs3
+--
+-- would represent three outgoing edges,
+-- one would be labelled with e1,
+-- the other would be labelled with e2,
+-- and one would be saying "anything else"
+
+emptyTransitions :: Transitions CAState
+emptyTransitions =
+  MkTransitions Map.empty (MkCAState [])
+
+mergeTransitions :: Transitions CAState -> Transitions CAState -> Transitions CAState
+mergeTransitions (MkTransitions m1 d1) (MkTransitions m2 d2) =
+  MkTransitions
+    (Map.merge
+      (Map.mapMissing (const (<> d2)))
+      (Map.mapMissing (const (d1 <>)))
+      (Map.zipWithMatched (const (<>)))
+      m1 m2
+    ) (d1 <> d2)
+
+allResiduals :: Clause -> Transitions CAState
+allResiduals Top                    = MkTransitions Map.empty topState
+allResiduals Bottom                 = MkTransitions Map.empty bottomState
+allResiduals (Must stateOfAffairs)  =
+  MkTransitions (Map.singleton stateOfAffairs topState) bottomState
+allResiduals (May _)                = MkTransitions Map.empty topState -- top, following the paper
+allResiduals (Shant stateOfAffairs) =
+  MkTransitions (Map.singleton stateOfAffairs bottomState) topState
+allResiduals (If GTrue clause)      =
+  MkTransitions Map.empty (MkCAState [clause])
+allResiduals (If guard clause)      =
+  MkTransitions (Map.fromList ((\ e -> (e, MkCAState [clause])) <$> eventsSatisfying guard)) topState -- top, following the paper
+
+-- | TODO: this has to be made more clever
+eventsSatisfying :: Guard -> [Event]
+eventsSatisfying (GDone e) = [e]
+eventsSatisfying (GNot _g) = [] -- TODO: this is wrong
+eventsSatisfying GTrue     = [] -- this is fine, handled via default
+eventsSatisfying GFalse    = []
+
+allResidualsClauses :: [Clause] -> Transitions CAState
+allResidualsClauses clauses =
+  foldl' mergeTransitions emptyTransitions (allResiduals <$> clauses)
+
+normalise :: [Clause] -> [Clause]
+normalise clauses =
+  let
+    r = filter (/= Top) (nubOrd (sort clauses))
+  in
+    if Bottom `elem` r
+      then [Bottom]
+      else r
+
+normaliseState :: CAState -> CAState
+normaliseState = coerce normalise
+
+normaliseTransitions :: Transitions CAState -> Transitions CAState
+normaliseTransitions (MkTransitions m d) =
+  MkTransitions (normaliseState <$> m) (normaliseState d)
+
+locationsFromTransitions :: Transitions CAState -> [CAState]
+locationsFromTransitions (MkTransitions m d) =
+  nubOrd (d : Map.elems m)
+
+explore :: [CAState] -> [CAState] -> [(CAState, Transitions CAState)]
+explore []       _visited = []
+explore (s : ss)  visited
+  | s `elem` visited      = explore ss visited
+  | otherwise             =
+    let
+      r = normaliseTransitions (allResidualsClauses (coerce s))
+    in
+      (s, r) : explore (locationsFromTransitions r <> ss) (s : visited)
+
+buildAutomaton :: CAState -> Aut CAState
+buildAutomaton initial =
+  MkAut (explore [initial] [])
+
+data Aut s =
+  MkAut { unAut :: [(s, Transitions s)] }
+  deriving (Functor)
+
+instance Show s => Show (Aut s) where
+  show (MkAut ts) =
+    unlines (map renderState ts)
+
+renderState :: Show s => (s, Transitions s) -> String
+renderState (s, ts) =
+  "State " <> show s <> ":\n" <> unlines (map ("  " <>) (renderTransitions ts))
+
+renderTransitions :: Show s => Transitions s -> [String]
+renderTransitions (MkTransitions m d) =
+  let
+    xs = Map.toList m
+  in
+    map (\ (e, s) -> show e <> " -> " <> show s) xs ++ ["default -> " <> show d]
+
+renameAutomaton :: Aut CAState -> Aut Int
+renameAutomaton original@(MkAut o) =
+  let
+    stateMap :: Map CAState Int
+    stateMap = Map.fromList (zip (fst <$> o) [0 ..])
+  in
+    (stateMap Map.!) <$> original
+
 {- | Residual at the level of *clauses* (as opposed to contracts / sequences of clauses).
   NOTE: I depart from the paper by simplifying this to use only one event/action as opposed to a set/list of them
 -}
-residual' :: Clause -> Event -> Clause
+residual' :: Clause -> (Event -> Clause)
 residual' = flip flippedResidual'
   where
     flippedResidual' :: Event -> Clause -> Clause
@@ -84,7 +215,7 @@ residual' = flip flippedResidual'
           if actualEvent `matches` stateOfAffairs
           then Top
           else Bottom
-        mc@(May _)            -> mc
+        mc@(May _)            -> mc -- Top in the paper
         Shant stateOfAffairs  ->
           if actualEvent `matches` stateOfAffairs
           then Bottom

experiments/contract-automata/src/Examples.hs

@@ -141,6 +141,34 @@ bankExampleTrace = [eventJohnLogin, eventHackAttempt]
 autBankExample :: ContractAutomaton
 autBankExample = mkContractAut (contractToCAState contractBank) residualWithoutSimplify
 
+autBankExample' :: Aut Int
+autBankExample' = renameAutomaton (buildAutomaton (contractToCAState contractBank))
+
+-- >>> autBankExample'
+-- State 0:
+--   MkEvent {getActor = MkParty {getName = "Hacker"}, getAction = "attemptHack"} -> 2
+--   MkEvent {getActor = MkParty {getName = "John"}, getAction = "login"} -> 5
+--   default -> 1
+-- <BLANKLINE>
+-- State 1:
+--   default -> 1
+-- <BLANKLINE>
+-- State 2:
+--   MkEvent {getActor = MkParty {getName = "Bank"}, getAction = "resolveSituation"} -> 3
+--   MkEvent {getActor = MkParty {getName = "John"}, getAction = "login"} -> 4
+--   MkEvent {getActor = MkParty {getName = "John"}, getAction = "makeMoneyTransfers"} -> 4
+--   default -> 1
+-- <BLANKLINE>
+-- State 3:
+--   default -> 1
+-- <BLANKLINE>
+-- State 4:
+--   default -> 4
+-- <BLANKLINE>
+-- State 5:
+--   default -> 1
+-- <BLANKLINE>
+
 runBankExampleOnTrace :: Trace -> Identity CAState
 runBankExampleOnTrace = run autBankExample.aut