Add permissibility function

Finding the possible calls seems broken though

src/elm/CallSequence/CallSequence.elm

@@ -3,7 +3,11 @@ module CallSequence.CallSequence exposing (..)
 import List exposing (head)
 import GossipGraph.Agent exposing (AgentId)
 import GossipGraph.Call exposing (Call, includes)
-import GossipGraph.Relation exposing (Kind(..))
+import GossipGraph.Relation as Relation exposing (Kind(..))
+import Graph
+import IntDict
+import List.Extra exposing (mapAccumr)
+import GossipGraph.Call as Call
 
 
 {-| A list of consecutive calls. Ordered latest to first call to improve lookup speed.
@@ -25,4 +29,4 @@ containing sequence agent =
                 call :: containing calls agent
 
             else
-                containing calls agent
+                containing calls agent

src/elm/GossipProtocol/GossipProtocol.elm

@@ -1,10 +1,12 @@
 module GossipProtocol.GossipProtocol exposing (..)
 
-import Graph exposing (Graph, NodeContext, fold)
-import GossipGraph.Agent exposing (Agent, AgentId)
-import GossipGraph.Call exposing (Call)
 import CallSequence.CallSequence exposing (CallSequence)
-import GossipGraph.Relation as Relation exposing (Kind(..), Relation)
+import GossipGraph.Agent exposing (Agent, AgentId)
+import GossipGraph.Call as Call exposing (Call)
+import GossipGraph.Relation as Relation exposing (Kind(..), Relation, knows)
+import Graph exposing (Graph, NodeContext)
+import IntDict
+import List.Extra exposing (mapAccumr)
 
 
 {-| Protocol conditions
@@ -18,8 +20,8 @@ type alias ProtocolCondition =
 Select x, y ∈ A, such that x ≠ y, Nxy, and π(x, y)
 
 -}
-select : Graph Agent Relation -> ProtocolCondition -> CallSequence -> List Call
-select graph condition sequence =
+selectCalls : Graph Agent Relation -> ProtocolCondition -> CallSequence -> List Call
+selectCalls graph condition sequence =
     let
         calls : NodeContext Agent Relation -> List Call -> List Call
         calls context acc =
@@ -28,7 +30,7 @@ select graph condition sequence =
                 localRelations =
                     -- select x, y ∈ A, such that x /= y, Nxy
                     Relation.fromNodeContext context
-                    |> List.filter (\{ from, to } -> from /= to )
+                        |> List.filter (\{ from, to } -> from /= to)
 
                 -- the protocol condition needs a pair (x,y)
                 relationPairs =
@@ -38,9 +40,50 @@ select graph condition sequence =
             -- check π(x, y)
             -- the resulting list of calls is the list of calls that can be executed on G given the call history
             List.filter (\x -> condition x localRelations sequence) relationPairs
-                |> List.map GossipGraph.Call.fromTuple
+                |> List.map Call.fromTuple
                 |> (++) acc
     in
     Graph.fold calls [] graph
 
 
+{-| Given a call sequence, a graph and a protocol condition, figure out whether
+the call sequence is permitted.
+
+Call sequence σ;xy is P-permitted on G iff σ is P-permitted on G and xy is P-permitted on Gσ
+
+-}
+sequencePermittedOn : ProtocolCondition -> Graph Agent Relation -> CallSequence -> Bool
+sequencePermittedOn condition graph sequence =
+    let
+        relations : Graph Agent Relation -> List Relation
+        relations g =
+            Graph.edges g
+                |> List.map .label
+
+        isCallPermitted : Call -> Graph Agent Relation -> CallSequence -> Bool
+        isCallPermitted { from, to } currentGraph callHistory =
+            let
+                rels =
+                    relations currentGraph
+            in
+            from
+                /= to
+                -- N^σ xy
+                && List.any (\r -> knows from to Number r) rels
+                -- π(x, y)
+                && condition ( from, to ) rels callHistory
+    in
+    -- results in a tuple of the form ((Bool, (CallSequence, Graph Agent Relation)), List Graph Agent Relation)
+    -- Since the empty call sequence is allowed, start with true
+    -- while traversing the call sequence, we need to keep track of
+    -- - the calls that have occured so far
+    -- - the current state of the graph
+    -- - whether the current call was permitted
+    List.foldr (\call (history, state, permitted) ->
+        (call :: history
+        , Call.execute state call
+        , permitted && isCallPermitted call state history
+        )
+    ) ([], graph, True) sequence
+        |> Debug.log "result idk"
+        |> \(_, _, isPermitted) -> isPermitted

src/elm/Main.elm

@@ -21,6 +21,7 @@ import Html.Attributes exposing (..)
 import Html.Events exposing (..)
 import Json.Decode as Json
 import GossipGraph.Parser
+import CallSequence.CallSequence
 
 
 
@@ -232,6 +233,14 @@ callSequenceView model =
                 model.callSequence
                 model.agents
             )
+        , div [] [
+            case (model.graph, model.callSequence) of
+                (Ok graph, Ok sequence) ->
+                    GossipProtocol.sequencePermittedOn model.protocolCondition graph sequence
+                        |> (\b -> text <| "This sequence is " ++ (if b then "" else "not") ++ " permitted in protocol " ++ model.protocolName)
+                _ ->
+                    text <| "This sequence is not permitted in protocol " ++ model.protocolName
+        ]
         ]
 
 
@@ -263,7 +272,7 @@ protocolView model =
                         (Ok sequence, Ok agents, Ok graph) ->
                             let
                                 calls =
-                                    GossipProtocol.select graph model.protocolCondition sequence
+                                    GossipProtocol.selectCalls graph model.protocolCondition sequence
                             in
                             if List.isEmpty calls then
                                 [ text "No more calls are possible." ]