Attempt communicating between nodes

Elixir.hs

@@ -9,11 +9,11 @@ import Helpers
 import Snippets
 
 generate :: Spec -> DistributionConfig -> [(String, ElixirCode)]
-generate (Spec m i n ds) (Config ps _shared) =
+generate (Spec m i n ds) (Config ps shared) =
   let defs = filter (not . (specialDef i n)) ds
       cs = findConstants ds
       vs = findVariables ds
-      header = moduleHeader (moduleName m) m False
+      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
@@ -29,11 +29,12 @@ generateStarter (Spec m i _ ds) =
 generateForProcess ::
      Module -> String -> [Constant] -> [Variable] -> [Definition] -> ProcessConfig -> (String, ElixirCode)
 generateForProcess m n cs 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)))
+  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)
 
+
 filterDefs :: [Call] -> [Definition] -> [Definition]
 filterDefs is ds =
   let actionNames = map fst is
@@ -46,7 +47,7 @@ spec h cs vs ds dn =
   let g = map (\c -> (c, "const")) cs ++ map (\v -> (v, "variable")) vs
    in concat
         [ h
-        , ident (concat [constants cs, mapAndJoin (definition g) ds, "\n", next g dn, mainFunction, decideAction])
+        , ident (concat [constants cs, mapAndJoin (definition g) ds, "\n", next g dn, mainFunction, decideAction, waitLockFunction])
         , "\nend\n\n"
         ]
 

Helpers.hs

@@ -9,22 +9,28 @@ import Head
 import Snippets
 
 -- (MOD) helpers
-moduleHeader name (Module m doc) imp =
+moduleHeader name (Module m doc) shared imp =
   "defmodule " ++
   name ++
   " do\n" ++
   ident
     (moduleDoc doc ++
+     sharedVariablesDeclaration shared ++
      oracleDelaration ++
      if imp
        then "import " ++ m ++ "\n\n"
        else "")
 
+sharedVariablesDeclaration :: [String] -> String
+sharedVariablesDeclaration [] = ""
+sharedVariablesDeclaration shared =
+  unlines ([ "def shared_variables do", "  [" ] ++ map (\v -> "    :" ++ v ++ ",") shared ++ ["  ]", "end"])
+
 moduleContext (Module m _) = [(m, "module")]
 
 -- (CALL) helpers
 call i [] = snake i
-call i ps = snake i ++ "(" ++ intercalate ", " (ps) ++ ")"
+call i ps = snake i ++ "(" ++ intercalate ", " ps ++ ")"
 
 -- (IF) helpers
 ifExpr c t e = "(if " ++ c ++ ", do: " ++ t ++ ", else: " ++ e ++ ")"

Snippets.hs

@@ -28,9 +28,11 @@ decideAction =
 
 mainFunction =
   unlines
-    [ "def main(oracle, variables, step) do"
-    , "  IO.puts(inspect(variables))"
+    [ "def main(oracle, private_variables, step) do"
+    , "  shared_state = wait_lock(oracle)"
+    , "  variables = Map.merge(private_variables, shared_state)"
     , ""
+    , "  IO.puts(inspect(variables))"
     , "  actions = next(variables)"
     , ""
     , "  next_variables = decide_action(oracle, actions, step)"
@@ -40,6 +42,17 @@ mainFunction =
     , "end"
     ]
 
+waitLockFunction =
+  unlines
+    [ "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)"
+    , "  end"
+    , "end"
+    ]
+
 logState = "IO.puts (inspect variables)\n\n"
 
 oracleDelaration = "require Oracle\n\n"

elixir/lib/generated_code/apaew_d840.ex

@@ -0,0 +1,166 @@
+defmodule APAEWD840 do
+  def shared_variables do
+    [
+      :tcolor,
+      :tpos,
+      :active,
+    ]
+  end
+  require Oracle
+  @n "<value for N>"
+  def n, do: @n
+
+
+  def max_n(variables) do
+    20
+  end
+
+
+  def color(variables) do
+    MapSet.new(["white", "black"])
+  end
+
+
+  def const_init4(variables) do
+    MapSet.member?(MapSet.new([4]), @n)
+  end
+
+
+  def const_init10(variables) do
+    MapSet.member?(MapSet.new([10]), @n)
+  end
+
+
+  def const_init_all20(variables) do
+    MapSet.member?(2..50, @n)
+  end
+
+
+  def nodes(variables) do
+    Enum.filter(0..max_n(variables), fn(i) -> i < @n end)
+  end
+
+
+  def initiate_probe_condition(variables) do
+    Enum.all?([variables[:tpos] == 0, variables[:tcolor] == "black" or variables[:color][0] == "black"])
+  end
+
+  def initiate_probe(variables) do
+    %{
+      tpos: @n - 1,
+      tcolor: "white",
+      active: variables[:active],
+      color: Map.put(variables[:color], {0}, "white")
+    }
+  end
+
+
+  def pass_token_condition(variables, i) do
+    Enum.all?([variables[:tpos] == i, not variables[:active][i] or variables[:color][i] == "black" or variables[:tcolor] == "black"])
+  end
+
+  def pass_token(variables, i) 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")
+    }
+  end
+
+
+  def deactivate_condition(variables, i) do
+    variables[:active][i]
+  end
+
+  def deactivate(variables, i) do
+    %{
+      active: Map.put(variables[:active], {i}, false),
+      color: variables[:color],
+      tpos: variables[:tpos],
+      tcolor: variables[:tcolor]
+    }
+  end
+
+
+  def vars(variables) do
+    {variables[:active], variables[:color], variables[:tpos], variables[:tcolor]}
+  end
+
+
+  def token_always_black(variables) do
+    variables[:tcolor] == "black"
+  end
+
+
+  def termination_detected(variables) do
+    variables[:tpos] == 0 and variables[:tcolor] == "white" and variables[:color][0] == "white" and not variables[:active][0]
+  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

@@ -15,9 +15,11 @@ defmodule APAEWD840_node0 do
     ])
   end
 
-  def main(oracle, variables, step) do
-    IO.puts(inspect(variables))
+  def main(oracle, private_variables, step) do
+    shared_state = wait_lock(oracle)
+    variables = Map.merge(private_variables, shared_state)
 
+    IO.puts(inspect(variables))
     actions = next(variables)
 
     next_variables = decide_action(oracle, actions, step)
@@ -47,5 +49,12 @@ defmodule APAEWD840_node0 do
         Enum.at(possible_actions, n)[:state]
     end
   end
+  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)
+    end
+  end
 end
 

elixir/lib/generated_code/apaew_d840_node1.ex

@@ -15,9 +15,11 @@ defmodule APAEWD840_node1 do
     ])
   end
 
-  def main(oracle, variables, step) do
-    IO.puts(inspect(variables))
+  def main(oracle, private_variables, step) do
+    shared_state = wait_lock(oracle)
+    variables = Map.merge(private_variables, shared_state)
 
+    IO.puts(inspect(variables))
     actions = next(variables)
 
     next_variables = decide_action(oracle, actions, step)
@@ -47,5 +49,12 @@ defmodule APAEWD840_node1 do
         Enum.at(possible_actions, n)[:state]
     end
   end
+  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)
+    end
+  end
 end
 

elixir/lib/generated_code/apaew_d840_node2.ex

@@ -15,9 +15,11 @@ defmodule APAEWD840_node2 do
     ])
   end
 
-  def main(oracle, variables, step) do
-    IO.puts(inspect(variables))
+  def main(oracle, private_variables, step) do
+    shared_state = wait_lock(oracle)
+    variables = Map.merge(private_variables, shared_state)
 
+    IO.puts(inspect(variables))
     actions = next(variables)
 
     next_variables = decide_action(oracle, actions, step)
@@ -47,5 +49,12 @@ defmodule APAEWD840_node2 do
         Enum.at(possible_actions, n)[:state]
     end
   end
+  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)
+    end
+  end
 end
 

elixir/lib/mix/tasks/apaew_d840_node0.ex

@@ -0,0 +1,28 @@
+defmodule Mix.Tasks.ApaewD840Node0 do
+  @moduledoc "Printed when the user requests `mix help echo`"
+  @shortdoc "Echoes arguments"
+  use Mix.Task
+  import APAEWD840
+  import APAEWD840_node0
+
+  @impl Mix.Task
+  def run(args) do
+     variables = %{}
+      initial_state = %{
+  active: MapSet.new(nodes(variables), fn(n) -> true end),
+  color: MapSet.new(nodes(variables), fn(n) -> "white" end),
+  tpos: 0,
+  tcolor: "black"
+}
+
+    oracle_host = String.to_atom(Enum.at(args, 0))
+    IO.inspect(oracle_host)
+    result = Node.connect(oracle_host)
+    IO.inspect(result)
+    IO.inspect(Node.ping(oracle_host))
+    oracle = :global.whereis_name("oracle")
+    IO.puts(inspect(oracle))
+    main(oracle, initial_state, 0)
+
+  end
+end

elixir/lib/mix/tasks/apaew_d840_starter.ex

@@ -15,7 +15,10 @@ defmodule Mix.Tasks.ApaewD840Starter do
 }
 
     oracle = spawn(RandomOracle, :start, [initial_state, 0, nil])
-    :global.register_name("oracle", oracle)
+    a = :global.register_name("oracle", oracle)
+    IO.puts(inspect(a))
+    aoracle = :global.whereis_name("oracle")
+    IO.puts(inspect(aoracle))
 
     ref = Process.monitor(oracle)