Fix generation for the EWD840 spec

ConfigParser.hs

@@ -10,8 +10,6 @@ import Data.Aeson
 import qualified Data.ByteString.Lazy as B
 import GHC.Generics
 
-type Call = (String, [H.Value])
-
 jsonFile :: FilePath
 jsonFile = "config-sample.json"
 
@@ -20,7 +18,7 @@ data DistributionConfig =
   deriving (Show, Generic)
 
 data ProcessConfig =
-  PConfig String [Call]
+  PConfig String [H.Action]
   deriving (Show, Generic)
 
 instance FromJSON DistributionConfig where
@@ -35,8 +33,8 @@ instance FromJSON ProcessConfig where
     withObject "ProcessConfig" $ \obj -> do
       i <- obj .: "process_id"
       as <- obj .: "actions"
-      case mapM parseCall as of
-        Left e -> fail ("Invalid action calls in:" ++ show as ++ ". Error: " ++ show e)
+      case mapM parseState as of
+        Left e -> fail ("Invalid action in:" ++ show as ++ ". Error: " ++ show e)
         Right cs -> return (PConfig i cs)
 
 parseConfig :: FilePath -> IO (Either String DistributionConfig)

Elixir.hs

@@ -16,7 +16,7 @@ generate (Spec m i n ds) (Config ps shared) =
       header = moduleHeader (moduleName m) m shared False
       -- defNext = findIdentifier n ds
       base = baseSpec header cs vs defs
-   in (moduleName m, base):map (generateForProcess m n cs vs defs) ps
+   in (moduleName m, base):map (generateForProcess m n vs defs) ps
 
 generateStarter :: Spec -> (String, ElixirCode)
 generateStarter (Spec m i _ ds) =
@@ -27,18 +27,18 @@ generateStarter (Spec m i _ ds) =
    in (moduleName m, starterTask (moduleName m) state)
 
 generateForProcess ::
-     Module -> String -> [Constant] -> [Variable] -> [Definition] -> ProcessConfig -> (String, ElixirCode)
-generateForProcess m n cs vs defs (PConfig p as) =
+     Module -> String -> [Variable] -> [Definition] -> ProcessConfig -> (String, ElixirCode)
+generateForProcess m n vs defs (PConfig p as) =
   let name = moduleName m ++ "_" ++ p
       header = moduleHeader name m [] True
-      defNext = ActionDefinition n [] [] (ActionOr (map (\(i, ps) -> ActionCall i ps) as))
-   in (name, spec header cs vs [] defNext)
+      defNext = ActionDefinition n [] [] (ActionOr as)
+   in (name, spec header [] vs [] defNext)
 
 
-filterDefs :: [Call] -> [Definition] -> [Definition]
-filterDefs is ds =
-  let actionNames = map fst is
-   in filter (\d -> name d `elem` actionNames) ds
+-- filterDefs :: [Call] -> [Definition] -> [Definition]
+-- filterDefs is ds =
+--   let actionNames = map fst is
+   -- in filter (\d -> name d `elem` actionNames) ds
 
 {-- \vdash --}
 -- (MOD)
@@ -148,12 +148,12 @@ listActions g as =
   let infos = map (actionInfo g) as
    in "List.flatten([\n" ++ ident (intercalate ",\n" infos) ++ "\n])\n"
 
-decide :: Context -> [Action] -> ElixirCode
-decide _ [] = ""
-decide g as =
-  let infos = map (actionInfo g) as
-      list = "List.flatten([\n" ++ ident (intercalate ",\n" infos) ++ "\n])\n"
-   in "(\n" ++ ident ("decide_action(\n" ++ ident list ++ "\n)\n") ++ "\n)"
+-- decide :: Context -> [Action] -> ElixirCode
+-- decide _ [] = ""
+-- decide g as =
+--   let infos = map (actionInfo g) as
+--       list = "List.flatten([\n" ++ ident (intercalate ",\n" infos) ++ "\n])\n"
+--    in "(\n" ++ ident ("decide_action(\n" ++ ident list ++ "\n)\n") ++ "\n)"
 
 {-- \vdash_a --}
 action :: Context -> Action -> ElixirCode
@@ -204,7 +204,7 @@ value g (Union s (Set [v])) = "MapSet.put(" ++ value g s ++ ", " ++ value g v ++
 value g (Union s1 s2) = "MapSet.union(" ++ value g s1 ++ ", " ++ value g s2 ++ ")"
 -- [new] (SET-FILT)
 value g (Filtered i v p) =
-  "Enum.filter(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param") : g) p ++ " end)"
+  "MapSet.new(Enum.filter(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param") : g) p ++ " end))"
 -- [new] (SET-CAR)
 value g (Cardinality s) = "Enum.count(" ++ value g s ++ ")"
 value g (SetIn v s) = "MapSet.member?(" ++ value g s ++ ", " ++ value g v ++ ")"
@@ -220,12 +220,13 @@ value g (Record rs) =
 -- (REC-EXCEPT)
 value g (Except i es) =
   intercalate "\n" (map (\(k, v) -> "Map.put(" ++ reference g i ++ ", " ++ value g k ++ ", " ++ value g v ++ ")") es)
-value g (FunGen i s v) = "MapSet.new(" ++ value g s ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param") : g) v ++ " end)"
+value g (FunGen i s v) = "Map.new(" ++ value g s ++ ", fn(" ++ i ++ ") -> {" ++ i ++ ", " ++ value ((i, "param") : g) v ++ "} end)"
 -- [new] (CASE)
 value g (Case ms) = "cond do\n" ++ intercalate "\n" (map (caseMatch g) ms) ++ "\nend\n"
 -- Others, not specified
 value g (Range n1 n2) = value g n1 ++ ".." ++ value g n2
 value g (Ref i) = reference g i
+value g (Tuple [a]) = value g a
 value g (Tuple as) = "{" ++ intercalate ", " (map (value g) as) ++ "}"
 value g (Neg a) = "-" ++ value' g a
 value g (Add a b) = value' g a ++ " + " ++ value' g b

Parser.hs

@@ -37,8 +37,6 @@ parseTla a = do f <- readFile a
                 let e = parse specification "Error:" f
                 return (left show e)
 
-parseCall c = parse call ("Error parsing " ++ c ++ ":") c
-
 parseState s = parse action ("Error parsing " ++ s ++ ":") s
 
 parseTrace t = parse trace ("Error parsing " ++ t ++ ":") t
@@ -147,16 +145,16 @@ andAction = do string "/\\"
                ws
                return a
 
-action =  do string "IF"
-             ws
-             p <- predicate
-             string "THEN"
-             ws
-             at <- action
-             string "ELSE"
-             ws
-             af <- action
-             return (ActionIf p at af)
+action =  do try $ do string "IF"
+                      ws
+                      p <- predicate
+                      string "THEN"
+                      ws
+                      at <- action
+                      string "ELSE"
+                      ws
+                      af <- action
+                      return (ActionIf p at af)
          <|>
          do {Condition <$> predicate;}
          <|>

Snippets.hs

@@ -37,6 +37,7 @@ mainFunction =
     , ""
     , "  next_variables = decide_action(oracle, actions, step)"
     , "  send(oracle, {:notify, step, variables, next_variables})"
+    , "  Process.sleep(2000)"
     , ""
     , "  main(oracle, next_variables, step + 1)"
     , "end"
@@ -47,8 +48,8 @@ waitLockFunction =
     [ "def wait_lock(oracle) do"
     , "  send(oracle, {:lock, self()})"
     , "  receive do"
-    , "    {:ok, state} -> Map.split(state, shared_variables)"
-    , "    {:already_locked, _} -> Process.sleep(1000); wait_lock(oracle)"
+    , "    {:lock_acquired, state} -> IO.puts(\"Lock acquired\"); {map, _} = Map.split(state, shared_variables); map"
+    , "    {:already_locked, _} -> IO.puts(\"Lock refused\"); Process.sleep(1000); wait_lock(oracle)"
     , "  end"
     , "end"
     ]

config-sample.json

@@ -3,24 +3,24 @@
     {
       "process_id": "node0",
       "actions": [
-        "InitiateProbe",
-        "SendMsg(0)",
+        "InitiateProbe()",
+        "\\E i \\in {1, 2} : SendMsg(0, i)",
         "Deactivate(0)"
       ]
     },
     {
       "process_id": "node1",
       "actions": [
         "PassToken(1)",
-        "SendMsg(1)",
+        "\\E i \\in {0, 2} : SendMsg(1, i)",
         "Deactivate(1)"
       ]
     },
     {
       "process_id": "node2",
       "actions": [
         "PassToken(2)",
-        "SendMsg(2)",
+        "\\E i \\in {0, 1} : SendMsg(2, i)",
         "Deactivate(2)"
       ]
     }

elixir/lib/generated_code/apaew_d840.ex

@@ -37,7 +37,7 @@ defmodule APAEWD840 do
 
 
   def nodes(variables) do
-    Enum.filter(0..max_n(variables), fn(i) -> i < @n end)
+    MapSet.new(Enum.filter(0..max_n(variables), fn(i) -> i < @n end))
   end
 
 
@@ -50,7 +50,7 @@ defmodule APAEWD840 do
       tpos: @n - 1,
       tcolor: "white",
       active: variables[:active],
-      color: Map.put(variables[:color], {0}, "white")
+      color: Map.put(variables[:color], 0, "white")
     }
   end
 
@@ -64,7 +64,21 @@ defmodule APAEWD840 do
       tpos: i - 1,
       tcolor: (if variables[:color][i] == "black", do: "black", else: variables[:tcolor]),
       active: variables[:active],
-      color: Map.put(variables[:color], {i}, "white")
+      color: Map.put(variables[:color], i, "white")
+    }
+  end
+
+
+  def send_msg_condition(variables, i, j) do
+    variables[:active][i]
+  end
+
+  def send_msg(variables, i, j) do
+    %{
+      active: Map.put(variables[:active], j, true),
+      color: Map.put(variables[:color], i, (if j > i, do: "black", else: variables[:color][i])),
+      tpos: variables[:tpos],
+      tcolor: variables[:tcolor]
     }
   end
 
@@ -75,7 +89,7 @@ defmodule APAEWD840 do
 
   def deactivate(variables, i) do
     %{
-      active: Map.put(variables[:active], {i}, false),
+      active: Map.put(variables[:active], i, false),
       color: variables[:color],
       tpos: variables[:tpos],
       tcolor: variables[:tcolor]
@@ -98,68 +112,11 @@ defmodule APAEWD840 do
   end
 
 
-  def system_condition(variables) do
-    Enum.any?([initiate_probe_condition(variables), Enum.any?(MapSet.difference(nodes(variables), MapSet.new([0])), fn (i) ->pass_token_condition(variables, i) end
-    )])
-  end
-
-  def system(variables) do
-    List.flatten([
-      %{ action: "InitiateProbe()", condition: initiate_probe_condition(variables), state: initiate_probe(variables) },
-      Enum.map(MapSet.difference(nodes(variables), MapSet.new([0])), fn (i) -> [
-        %{ action: "PassToken(#{inspect i})", condition: pass_token_condition(variables, i), state: pass_token(variables, i) }
-      ] end
-      )
-    ])
-  end
-
-
-  def send_msg_condition(variables, i) do
-    Enum.all?([variables[:active][i], Enum.any?(MapSet.difference(nodes(variables), MapSet.new([i])), fn (j) ->true end
-    )])
-  end
-
-  def send_msg(variables, i) do
-    Map.merge(
-      %{
-      tpos: variables[:tpos],
-      tcolor: variables[:tcolor]
-    },
-      List.flatten([
-        Enum.map(MapSet.difference(nodes(variables), MapSet.new([i])), fn (j) -> [
-          %{ action: "ActionAnd [Primed \"active\" \(Except \"active\" [\(Tuple [Ref \"j\"\],Lit \(Boolean True\)\)\]\),Primed \"color\" \(Except \"color\" [\(Tuple [Ref \"i\"\],If \(Gt \(Ref \"j\"\) \(Ref \"i\"\)\) \(Lit \(Str \"black\"\)\) \(Index \(Ref \"color\"\) \(Ref \"i\"\)\)\)\]\)\]", condition: true, state: %{
-            active: Map.put(variables[:active], {j}, true),
-            color: Map.put(variables[:color], {i}, (if j > i, do: "black", else: variables[:color][i]))
-          } }
-        ] end
-        )
-      ]))
-  end
-
-
   # "NeverChangeColor": OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "UNCHANGED" [NameEx "color"],OperEx "OPER_APP" [NameEx "vars"]]]
   # "TerminationDetection": OperEx "IMPLIES" [OperEx "OPER_APP" [NameEx "terminationDetected"],OperEx "FORALL3" [NameEx "i",OperEx "OPER_APP" [NameEx "Nodes"],OperEx "NOT" [OperEx "FUN_APP" [NameEx "active",NameEx "i"]]]]
   # "Liveness": OperEx "LEADS_TO" [OperEx "FORALL3" [NameEx "i",OperEx "OPER_APP" [NameEx "Nodes"],OperEx "NOT" [OperEx "FUN_APP" [NameEx "active",NameEx "i"]]],OperEx "OPER_APP" [NameEx "terminationDetected"]]
   # "FalseLiveness": OperEx "LEADS_TO" [OperEx "FORALL3" [NameEx "i",OperEx "OPER_APP" [NameEx "Nodes"],OperEx "GLOBALLY" [OperEx "EVENTUALLY" [OperEx "NOT" [OperEx "FUN_APP" [NameEx "active",NameEx "i"]]]]],OperEx "OPER_APP" [NameEx "terminationDetected"]]
   # "Inv": OperEx "OR" [OperEx "LABEL" [OperEx "FORALL3" [NameEx "i",OperEx "OPER_APP" [NameEx "Nodes"],OperEx "IMPLIES" [OperEx "LT" [NameEx "tpos",NameEx "i"],OperEx "NOT" [OperEx "FUN_APP" [NameEx "active",NameEx "i"]]]],ValEx (TlaStr "P0")],OperEx "LABEL" [OperEx "EXISTS3" [NameEx "j",OperEx "OPER_APP" [NameEx "Nodes"],OperEx "IMPLIES" [OperEx "AND" [OperEx "LE" [ValEx (TlaInt 0),NameEx "j"],OperEx "LE" [NameEx "j",NameEx "tpos"]],OperEx "EQ" [OperEx "FUN_APP" [NameEx "color",NameEx "j"],ValEx (TlaStr "black")]]],ValEx (TlaStr "P1")],OperEx "LABEL" [OperEx "EQ" [NameEx "tcolor",ValEx (TlaStr "black")],ValEx (TlaStr "P2")]]
-  def environment_condition(variables) do
-    Enum.any?(nodes(variables), fn (i) ->Enum.any?([send_msg_condition(variables, i), deactivate_condition(variables, i)]) end
-    )
-  end
-
-  def environment(variables) do
-    List.flatten([
-      Enum.map(nodes(variables), fn (i) -> [
-        %{ action: "SendMsg(#{inspect i})", condition: send_msg_condition(variables, i), state: send_msg(variables, i) },
-        %{ action: "Deactivate(#{inspect i})", condition: deactivate_condition(variables, i), state: deactivate(variables, i) }
-      ] end
-      )
-    ])
-  end
-
-
-  # "AllNodesTerminateIfNoMessages": OperEx "IMPLIES" [OperEx "EVENTUALLY" [OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "FORALL3" [NameEx "i",OperEx "OPER_APP" [NameEx "Nodes"],OperEx "NOT" [OperEx "OPER_APP" [NameEx "SendMsg",NameEx "i"]]],OperEx "OPER_APP" [NameEx "vars"]]]],OperEx "EVENTUALLY" [OperEx "FORALL3" [NameEx "i",OperEx "OPER_APP" [NameEx "Nodes"],OperEx "NOT" [OperEx "FUN_APP" [NameEx "active",NameEx "i"]]]]]
-  # "Spec": OperEx "AND" [OperEx "AND" [OperEx "OPER_APP" [NameEx "Init"],OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "OPER_APP" [NameEx "Next"],OperEx "OPER_APP" [NameEx "vars"]]]],OperEx "WEAK_FAIRNESS" [OperEx "OPER_APP" [NameEx "vars"],OperEx "OPER_APP" [NameEx "System"]]]
   # "SpecWFNext": OperEx "AND" [OperEx "AND" [OperEx "OPER_APP" [NameEx "Init"],OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "OPER_APP" [NameEx "Next"],OperEx "OPER_APP" [NameEx "vars"]]]],OperEx "WEAK_FAIRNESS" [OperEx "OPER_APP" [NameEx "vars"],OperEx "OPER_APP" [NameEx "Next"]]]
   # "CheckInductiveSpec": OperEx "AND" [OperEx "OPER_APP" [NameEx "Inv"],OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "OPER_APP" [NameEx "Next"],OperEx "OPER_APP" [NameEx "vars"]]]]
 end

elixir/lib/generated_code/apaew_d840_node0.ex

@@ -2,21 +2,19 @@ defmodule APAEWD840_node0 do
   require Oracle
 
   import APAEWD840
-  @n 3
-  def n, do: @n
-
-
 
   def next(variables) do
     List.flatten([
       %{ action: "InitiateProbe()", condition: initiate_probe_condition(variables), state: initiate_probe(variables) },
-      %{ action: "SendMsg(Lit (Num 0))", condition: send_msg_condition(variables, 0), state: send_msg(variables, 0) },
+      Enum.map(MapSet.new([1, 2]), fn (i) -> [
+        %{ action: "SendMsg(Lit (Num 0), #{inspect i})", condition: send_msg_condition(variables, 0, i), state: send_msg(variables, 0, i) }
+      ] end
+      ),
       %{ action: "Deactivate(Lit (Num 0))", condition: deactivate_condition(variables, 0), state: deactivate(variables, 0) }
     ])
   end
 
   def main(oracle, private_variables, step) do
-    IO.puts("Waiting lock")
     shared_state = wait_lock(oracle)
     variables = Map.merge(private_variables, shared_state)
 
@@ -25,6 +23,7 @@ defmodule APAEWD840_node0 do
 
     next_variables = decide_action(oracle, actions, step)
     send(oracle, {:notify, step, variables, next_variables})
+    Process.sleep(2000)
 
     main(oracle, next_variables, step + 1)
   end
@@ -50,14 +49,11 @@ defmodule APAEWD840_node0 do
         Enum.at(possible_actions, n)[:state]
     end
   end
-
   def wait_lock(oracle) do
-    IO.puts("sending lock request to:")
-    IO.inspect(oracle)
     send(oracle, {:lock, self()})
     receive do
-      {:ok, state} -> IO.puts("Lock acquired"); {map, _rest} = Map.split(state, shared_variables); map
-      {:already_locked, _} -> IO.puts("Oracle locked"); Process.sleep(1000); wait_lock(oracle)
+      {:lock_acquired, state} -> IO.puts("Lock acquired"); {map, _} = Map.split(state, shared_variables); map
+      {:already_locked, _} -> IO.puts("Lock refused"); Process.sleep(1000); wait_lock(oracle)
     end
   end
 end