Possibly hit bug in TLC graph generation :(

ConfigParser.hs

@@ -43,3 +43,6 @@ parseConfig file = do
   return (eitherDecode content)
 -- main :: IO ()
 -- main = parseJson jsonFile >>= print
+
+processNames :: DistributionConfig -> [String]
+processNames (Config ps _) = map (\(PConfig n _) -> n) ps

Elixir.hs

@@ -146,7 +146,7 @@ listActions :: Context -> [Action] -> ElixirCode
 listActions _ [] = ""
 listActions g as =
   let infos = map (actionInfo g) as
-   in "List.flatten([\n" ++ ident (intercalate ",\n" infos) ++ "\n])\n"
+   in "Enum.filter(\n  List.flatten([\n" ++ ident (intercalate ",\n" infos) ++ "\n]),\n  fn(action) -> action[:condition] end\n)"
 
 -- decide :: Context -> [Action] -> ElixirCode
 -- decide _ [] = ""
@@ -295,7 +295,7 @@ actionInfo g a =
 caseMatch g (Match p v) = value g p ++ " -> " ++ value g v
 caseMatch g (DefaultMatch v) = "true -> " ++ value g v
 
-mapping g ((Key i), v) = show i ++ ": " ++ value g v
+mapping g ((Key i), v) = lit i ++ " => " ++ value g v
 mapping g ((All i a), v) =
   let ig = (i, "param") : g
    in value g a ++ " |> Enum.map(fn (" ++ i ++ ") -> {" ++ i ++ ", " ++ value ig v ++ "} end)"

Snippets.hs

@@ -4,24 +4,23 @@ decideAction =
   unlines
     [ ""
     , "def decide_action(oracle, actions, step) do"
-    , "  possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end)"
-    , "  different_states = Enum.uniq_by(possible_actions, fn(action) -> action[:state] end)"
+    , "  different_states = Enum.uniq_by(actions, fn(action) -> action[:state] end)"
     , ""
     , "  cond do"
     , "    Enum.count(different_states) == 1 ->"
-    , "      Enum.at(possible_actions, 0)[:state]"
+    , "      Enum.at(actions, 0)[:state]"
     , "    Enum.empty?(different_states) ->"
     , "      IO.puts(\"DEADLOCK\")"
     , "      exit(0)"
     , "    true ->"
-    , "      send oracle, {:choose, self(), possible_actions}"
+    , "      send oracle, {:choose, self(), actions}"
     , ""
     , "      n = receive do"
     , "        {:ok, n} -> n"
     , "        {:stop} -> exit(0)"
     , "      end"
     , ""
-    , "      Enum.at(possible_actions, n)[:state]"
+    , "      Enum.at(actions, n)[:state]"
     , "  end"
     , "end"
     ]

StateGraphParser.hs

@@ -11,6 +11,7 @@ import Head as H
 import Elixir
 import Helpers
 import Parser
+import ConfigParser
 
 getJSON :: FilePath -> IO B.ByteString
 getJSON = B.readFile
@@ -45,14 +46,14 @@ instance FromJSON Node where
 instance FromJSON Edge where
   parseJSON (Object v) = Edge <$> v .: "tail" <*> v .: "head"
 
-genTests :: String -> Graph -> Either String String
-genTests m Graph {nodes = ns, edges = es} =
-  case traverse (testForNode m (Graph ns es)) ns of
+genTests :: String -> [String] -> Graph -> Either String String
+genTests m ms Graph {nodes = ns, edges = es} =
+  case traverse (testForNode (map ((m ++ "_") ++) ms) (Graph ns es)) ns of
     Right ts -> Right (header m ++ intercalate "\n" ts ++ "\nend")
     Left e -> Left e
 
-testForNode :: String -> Graph -> Node -> Either String String
-testForNode m g Node {nodeId = i, label = l} = do
+testForNode :: [String] -> Graph -> Node -> Either String String
+testForNode ms g Node {nodeId = i, label = l} = do
   vs <- toMap Node {nodeId = i, label = l}
   ss <- statesFromId g i >>= traverse toMap
   return
@@ -62,7 +63,7 @@ testForNode m g Node {nodeId = i, label = l} = do
        , ""
        , "  expectedStates = [" ++ intercalate ",\n" ss ++ "]"
        , ""
-       , "  actions = " ++ m ++ ".next(variables)"
+       , "  actions = List.flatten([" ++ intercalate ", " (map (++ ".next(variables)") ms) ++ "])"
        , "  states = Enum.map(actions, fn action -> action[:state] end)"
        , ""
        , "  assert Enum.sort(Enum.uniq(states)) == Enum.sort(Enum.uniq(expectedStates))"
@@ -71,7 +72,7 @@ testForNode m g Node {nodeId = i, label = l} = do
 
 statesFromId :: Graph -> Integer -> Either String [Node]
 statesFromId Graph {nodes = ns, edges = es} i =
-  let edgesFromId = filter (\Edge {nodeFrom = f, nodeTo = t} -> f == i) es
+  let edgesFromId = filter (\Edge {nodeFrom = f, nodeTo = _} -> f == i) es
       nodesIdsFromId = map (\Edge {nodeFrom = _, nodeTo = t} -> t) edgesFromId
    in traverse (findNode ns) nodesIdsFromId
 
@@ -108,13 +109,16 @@ header m = unlines ["defmodule " ++ m ++ "Test do", "  use ExUnit.Case", "  doct
 
 main :: IO ()
 main = do
-  (moduleName:file:_) <- getArgs
+  (moduleName:file:configFile:_) <- getArgs
+  config <- parseConfig configFile
   d <- (eitherDecode <$> getJSON file) :: IO (Either String Graph)
   case d of
     Left err -> putStrLn err
     Right ps ->
-      case genTests moduleName ps of
+      case fmap processNames config of
         Left err -> putStrLn err
-        Right s ->
-          let f = "elixir/test/generated_code/" ++ snake moduleName ++ "_test.exs"
-           in writeFile f s
+        Right ms -> case genTests moduleName ms ps of
+                      Left err -> putStrLn err
+                      Right s ->
+                        let f = "elixir/test/generated_code/" ++ snake moduleName ++ "_test.exs"
+                         in writeFile f s

elixir/lib/generated_code/apaew_d840_node0.ex

@@ -4,14 +4,17 @@ defmodule APAEWD840_node0 do
   import APAEWD840
 
   def next(variables) do
-    List.flatten([
+    Enum.filter(
+      List.flatten([
       %{ action: "InitiateProbe()", condition: initiate_probe_condition(variables), state: initiate_probe(variables) },
       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) }
-    ])
+    ]),
+      fn(action) -> action[:condition] end
+    )
   end
 
   def main(oracle, private_variables, step) do
@@ -29,24 +32,23 @@ defmodule APAEWD840_node0 do
   end
 
   def decide_action(oracle, actions, step) do
-    possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end)
-    different_states = Enum.uniq_by(possible_actions, fn(action) -> action[:state] end)
+    different_states = Enum.uniq_by(actions, fn(action) -> action[:state] end)
 
     cond do
       Enum.count(different_states) == 1 ->
-        Enum.at(possible_actions, 0)[:state]
+        Enum.at(actions, 0)[:state]
       Enum.empty?(different_states) ->
         IO.puts("DEADLOCK")
         exit(0)
       true ->
-        send oracle, {:choose, self(), possible_actions}
+        send oracle, {:choose, self(), actions}
 
         n = receive do
           {:ok, n} -> n
           {:stop} -> exit(0)
         end
 
-        Enum.at(possible_actions, n)[:state]
+        Enum.at(actions, n)[:state]
     end
   end
   def wait_lock(oracle) do

elixir/lib/generated_code/apaew_d840_node1.ex

@@ -4,14 +4,17 @@ defmodule APAEWD840_node1 do
   import APAEWD840
 
   def next(variables) do
-    List.flatten([
+    Enum.filter(
+      List.flatten([
       %{ action: "PassToken(Lit (Num 1))", condition: pass_token_condition(variables, 1), state: pass_token(variables, 1) },
       Enum.map(MapSet.new([0, 2]), fn (i) -> [
         %{ action: "SendMsg(Lit (Num 1), #{inspect i})", condition: send_msg_condition(variables, 1, i), state: send_msg(variables, 1, i) }
       ] end
       ),
       %{ action: "Deactivate(Lit (Num 1))", condition: deactivate_condition(variables, 1), state: deactivate(variables, 1) }
-    ])
+    ]),
+      fn(action) -> action[:condition] end
+    )
   end
 
   def main(oracle, private_variables, step) do
@@ -29,24 +32,23 @@ defmodule APAEWD840_node1 do
   end
 
   def decide_action(oracle, actions, step) do
-    possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end)
-    different_states = Enum.uniq_by(possible_actions, fn(action) -> action[:state] end)
+    different_states = Enum.uniq_by(actions, fn(action) -> action[:state] end)
 
     cond do
       Enum.count(different_states) == 1 ->
-        Enum.at(possible_actions, 0)[:state]
+        Enum.at(actions, 0)[:state]
       Enum.empty?(different_states) ->
         IO.puts("DEADLOCK")
         exit(0)
       true ->
-        send oracle, {:choose, self(), possible_actions}
+        send oracle, {:choose, self(), actions}
 
         n = receive do
           {:ok, n} -> n
           {:stop} -> exit(0)
         end
 
-        Enum.at(possible_actions, n)[:state]
+        Enum.at(actions, n)[:state]
     end
   end
   def wait_lock(oracle) do

elixir/lib/generated_code/apaew_d840_node2.ex

@@ -4,14 +4,17 @@ defmodule APAEWD840_node2 do
   import APAEWD840
 
   def next(variables) do
-    List.flatten([
+    Enum.filter(
+      List.flatten([
       %{ action: "PassToken(Lit (Num 2))", condition: pass_token_condition(variables, 2), state: pass_token(variables, 2) },
       Enum.map(MapSet.new([0, 1]), fn (i) -> [
         %{ action: "SendMsg(Lit (Num 2), #{inspect i})", condition: send_msg_condition(variables, 2, i), state: send_msg(variables, 2, i) }
       ] end
       ),
       %{ action: "Deactivate(Lit (Num 2))", condition: deactivate_condition(variables, 2), state: deactivate(variables, 2) }
-    ])
+    ]),
+      fn(action) -> action[:condition] end
+    )
   end
 
   def main(oracle, private_variables, step) do
@@ -29,24 +32,23 @@ defmodule APAEWD840_node2 do
   end
 
   def decide_action(oracle, actions, step) do
-    possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end)
-    different_states = Enum.uniq_by(possible_actions, fn(action) -> action[:state] end)
+    different_states = Enum.uniq_by(actions, fn(action) -> action[:state] end)
 
     cond do
       Enum.count(different_states) == 1 ->
-        Enum.at(possible_actions, 0)[:state]
+        Enum.at(actions, 0)[:state]
       Enum.empty?(different_states) ->
         IO.puts("DEADLOCK")
         exit(0)
       true ->
-        send oracle, {:choose, self(), possible_actions}
+        send oracle, {:choose, self(), actions}
 
         n = receive do
           {:ok, n} -> n
           {:stop} -> exit(0)
         end
 
-        Enum.at(possible_actions, n)[:state]
+        Enum.at(actions, n)[:state]
     end
   end
   def wait_lock(oracle) do