diff --git a/Elixir.hs b/Elixir.hs index b33f9ba..43198f3 100644 --- a/Elixir.hs +++ b/Elixir.hs @@ -12,9 +12,22 @@ generate :: Spec -> DistributionConfig -> [(String, ElixirCode)] generate (Spec m i n ds) (Config ps shared) = let defs = filter (not . (specialDef i n)) ds cs = findConstants ds vs = findVariables ds - defInit = findIdentifier i ds -- defNext = findIdentifier n ds - in map (\(PConfig p as) -> ((moduleName m) ++ "_" ++ p, spec m cs vs (filterDefs as defs) defInit (ActionDefinition n [] [] (ActionOr (map (\(i, ps) -> ActionCall i ps) as))))) ps + in map (generateForProcess m n cs vs defs) ps + +generateStarter :: Spec -> (String, ElixirCode) +generateStarter (Spec m i _ ds) = let cs = findConstants ds + vs = findVariables ds + g = map (\c -> (c, "const")) cs ++ map (\v -> (v, "variable")) vs + state = ini (g ++ moduleContext m) (findIdentifier i ds) + in (moduleName m, starterTask ((pascal . moduleName) m) state) + +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 + ds = filterDefs as defs + defNext = (ActionDefinition n [] [] (ActionOr (map (\(i, ps) -> ActionCall i ps) as))) + in (name, spec header cs vs ds defNext) filterDefs :: [Call] -> [Definition] -> [Definition] filterDefs is ds = let actionNames = map fst is @@ -22,20 +35,19 @@ filterDefs is ds = let actionNames = map fst is {-- \vdash --} -- (MOD) -spec :: Module -> [Constant] -> [Variable] -> [Definition] -> Init -> Next -> ElixirCode -spec m cs vs ds di dn = let g = map (\c -> (c, "const")) cs ++ map (\v -> (v, "variable")) vs - state = ini (g ++ moduleContext m) di - in concat [moduleHeader m, - ident (concat [ - constants cs, - mapAndJoin (definition g) ds, - "\n", - next g dn, - decideAction - ] - ), - "\nend\n\n", - mainCall m state] +spec :: String -> [Constant] -> [Variable] -> [Definition] -> Next -> ElixirCode +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 + ] + ), + "\nend\n\n"] {-- \vdash_const --} -- (CONST) @@ -87,13 +99,13 @@ actionsAndConditions g (Condition p) = ([value g p], []) -- [new] (EXT) actionsAndConditions g (Exists i v a) = let ig = (i, "param"):g (ics, _) = actionsAndConditions ig a - c = "Enum.any?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ "end\n)" + c = "Enum.any?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ " end\n)" in ([c], [decide g [a]]) -- [new]: must test actionsAndConditions g (ForAll i v a) = let ig = (i, "param"):g (ics, ias) = actionsAndConditions ig a - c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ "end\n)" + c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ " end\n)" in ([c], ias) -- (TRA) @@ -154,7 +166,7 @@ value g (And ps) = intercalate " and " (map (value g) ps) -- [new] (PRED-OR) value g (Or ps) = intercalate " or " (map (value g) ps) -value g (If c t e) = "if " ++ value g c ++ ", do: " ++ value g t ++ ", else: " ++ value g e +value g (If c t e) = "(if " ++ value g c ++ ", do: " ++ value g t ++ ", else: " ++ value g e ++ ")" -- [new] (PRED-ALL) value g (PForAll i v p) = "Enum.all?(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) p ++ " end)" @@ -189,7 +201,7 @@ value g (Record rs) = let (literals, generations) = partition isLiteral rs in if m == [] then l else m ++ " |> Enum.into(" ++ l ++ ")" -- (REC-EXCEPT) -value g (Except i es) = unlines (map (\(k,v) -> "Map.put(" ++ reference g i ++ ", " ++ value g k ++ ", " ++ value g v ++ ")") es) +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)" @@ -239,7 +251,7 @@ next :: Context -> Definition -> ElixirCode -- (NEXT) next g (ActionDefinition _ _ doc a) = let (_, actions) = actionsAndConditions g a - in funDoc doc ++ "def main(variables) do\n" ++ ident (logState ++ "main(" ++ (aFold actions)) ++ ")\nend\n" + in funDoc doc ++ "def next(variables) do\n" ++ ident (logState ++ "next(" ++ (aFold actions)) ++ ")\nend\n" {-- \vdash_i -} diff --git a/Helpers.hs b/Helpers.hs index fdd3130..184b658 100644 --- a/Helpers.hs +++ b/Helpers.hs @@ -10,12 +10,10 @@ import DocHandler import Snippets -- (MOD) helpers -moduleHeader (Module i doc) = "defmodule " ++ pascal i ++ " do\n" ++ ident (moduleDoc doc ++ oracleDelaration) +moduleHeader name (Module _ doc) = "defmodule " ++ pascal name ++ " do\n" ++ ident (moduleDoc doc ++ oracleDelaration) moduleContext (Module m _) = [(m,"module")] -mainCall (Module i _) s = pascal i ++ ".main(\n" ++ ident s ++ "\n)\n" - -- (CALL) helpers call i [] = snake i call i ps = snake i ++ "(" ++ intercalate ", " (ps) ++ ")" diff --git a/Main.hs b/Main.hs index 4218095..e6b5149 100644 --- a/Main.hs +++ b/Main.hs @@ -12,7 +12,11 @@ filename p = "elixir/lib/generated_code/" ++ snake p ++ ".ex" writeCode m (p, code) = let f = filename p in writeFile f code >> return f -convert name init next config (m, ds) = mapM (writeCode name) (generate (Spec m init next ds) config) +writeStarter (name, code) = let f = "elixir/lib/mix/tasks/" ++ snake name ++ "_starter.ex" in writeFile f code >> return f + +convert name init next config (m, ds) = do files <- mapM (writeCode name) (generate (Spec m init next ds) config) + starter <- writeStarter (generateStarter (Spec m init next ds)) + return (starter, files) main = do (mode:name:i:n:configFile:_) <- getArgs config <- parseConfig configFile diff --git a/Snippets.hs b/Snippets.hs index 1536bdc..41795e2 100644 --- a/Snippets.hs +++ b/Snippets.hs @@ -10,13 +10,14 @@ decideAction = unlines [ " Enum.count(different_states) == 1 ->", " Enum.at(possible_actions, 0)[:state]", " Enum.empty?(different_states) ->", - " %{}", + " IO.puts(\"DEADLOCK\")", + " exit(0)", " true ->", - " actions_names = Enum.map(possible_actions, fn(action) -> action[:action] end)", - " send @oracle, {self(), actions_names}", + " send oracle, {:choose, self(), possible_actions}", "", " n = receive do", " {:ok, n} -> n", + " {:stop} -> exit(0)", " end", "", " Enum.at(possible_actions, n)[:state]", @@ -24,6 +25,53 @@ decideAction = unlines [ "end" ] +mainFunction = unlines [ + "def main(oracle, variables, step) do", + " IO.puts(inspect(variables))", + "", + " actions = next(variables)", + "", + " next_variables = decide_action(oracle, actions, step)", + " send(oracle, {:notify, step, variables, next_variables})", + "", + " main(oracle, next_variables, step + 1)", + "end" + ] + logState = "IO.puts (inspect variables)\n\n" -oracleDelaration = "require Oracle\n@oracle spawn(Oracle, :start, [])\n\n\n" +oracleDelaration = "require Oracle\n\n" + +starterTask name init = unlines [ + "defmodule Mix.Tasks.Startmodel do", + " @moduledoc \"Printed when the user requests `mix help echo`\"", + " @shortdoc \"Echoes arguments\"", + " use Mix.Task", + "", + " @impl Mix.Task", + " def run(_) do", + " initial_state = " ++ init, + "", + " oracle = spawn(RandomOracle, :start, [])", + " " ++ name ++ ".main(oracle, initial_state, 0)", + " end", + "end" + ] + +tracerStarterTask name trace = unlines [ + "defmodule Mix.Tasks.Startmodel do", + " @moduledoc \"Printed when the user requests `mix help echo`\"", + " @shortdoc \"Echoes arguments\"", + " use Mix.Task", + "", + " @impl Mix.Task", + " def run(_) do", + " trace = [" + ] ++ trace ++ unlines [ + " ]", + "", + " oracle = spawn(TraceCheckerOracle, :start, [trace])", + " " ++ name ++ ".main(oracle, Enum.at(trace, 0), 0)", + " end", + "end" + ] diff --git a/elixir/lib/generated_code/apaew_d840.ex b/elixir/lib/generated_code/apaew_d840.ex deleted file mode 100644 index c09c999..0000000 --- a/elixir/lib/generated_code/apaew_d840.ex +++ /dev/null @@ -1,177 +0,0 @@ -defmodule ApaewD840 do - require Oracle - @oracle spawn(Oracle, :start, []) - - @n "" - def n, do: @n - - - def max_n_condition(variables) do - 20 - end - - - def color_condition(variables) do - MapSet.new(["white", "black"]) - end - - - def const_init4_condition(variables) do - MapSet.member?(MapSet.new([4]), @n) - end - - - def const_init10_condition(variables) do - MapSet.member?(MapSet.new([10]), @n) - end - - - def const_init_all20_condition(variables) do - MapSet.member?(2..50, @n) - end - - - def nodes_condition(variables) do - Enum.filter(0..max_n_condition(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) do - Enum.all?([variables[:tpos] == i(variables), not variables[:active][i(variables)] or variables[:color][i(variables)] == "black" or variables[:tcolor] == "black"]) - end - - def pass_token(variables) do - %{ - tpos: i(variables) - 1, - tcolor: if variables[:color][i(variables)] == "black", do: "black", else: variables[:tcolor], - active: variables[:active], - color: Map.put(variables[:color], {i(variables)}, "white") - } - end - - - def deactivate_condition(variables) do - variables[:active][i(variables)] - end - - def deactivate(variables) do - %{ - active: Map.put(variables[:active], {i(variables)}, false) - , - color: variables[:color], - tpos: variables[:tpos], - tcolor: variables[:tcolor] - } - end - - - def vars_condition(variables) do - {variables[:active], variables[:color], variables[:tpos], variables[:tcolor]} - end - - - def token_always_black_condition(variables) do - variables[:tcolor] == "black" - end - - - def termination_detected_condition(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 - initiate_probe_condition(variables) or Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([0])), fn(i) -> pass_token_condition(variables, i) end) - end - - - def send_msg_condition(variables) do - Enum.all?([variables[:active][i(variables)], Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([i(variables)])), fn (j) ->trueend - )]) - end - - def send_msg(variables) do - Map.merge( - %{ - tpos: variables[:tpos], - tcolor: variables[:tcolor] - }, - ( - decide_action( - List.flatten([ - %{ 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(variables)}, true) - , - color: Map.put(variables[:color], {i(variables)}, if j(variables) > i(variables), do: "black", else: variables[:color][i(variables)]) - } } - ]) - ) - )) - end - - - # OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "UNCHANGED" [NameEx "color"],OperEx "OPER_APP" [NameEx "vars"]]] - # 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"]]]] - # 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"]] - # 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"]] - # 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_condition(variables), fn(i) -> send_msg_condition(variables, i) or deactivate_condition(variables, i) end) - end - - - # 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"]]]]] - # 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"]]] - # 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"]]] - # OperEx "AND" [OperEx "OPER_APP" [NameEx "Inv"],OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "OPER_APP" [NameEx "Next"],OperEx "OPER_APP" [NameEx "vars"]]]] - def main(variables) do - IO.puts (inspect variables) - - main(%{}) - end - - def decide_action(actions) do - possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end) - different_states = Enum.uniq_by(possible_actions, fn(action) -> action[:state] end) - - cond do - Enum.count(different_states) == 1 -> - Enum.at(possible_actions, 0)[:state] - Enum.empty?(different_states) -> - %{} - true -> - actions_names = Enum.map(possible_actions, fn(action) -> action[:action] end) - send @oracle, {self(), actions_names} - - n = receive do - {:ok, n} -> n - end - - Enum.at(possible_actions, n)[:state] - end - end -end - -ApaewD840.main( - - %{ - active: MapSet.new(nodes_condition(variables), fn(n) -> true end), - color: MapSet.new(nodes_condition(variables), fn(n) -> "white" end), - tpos: 0, - tcolor: "black" - } -) diff --git a/elixir/lib/generated_code/apaew_d840_node0.ex b/elixir/lib/generated_code/apaew_d840_node0.ex index d1ca7ff..7b0a833 100644 --- a/elixir/lib/generated_code/apaew_d840_node0.ex +++ b/elixir/lib/generated_code/apaew_d840_node0.ex @@ -1,7 +1,5 @@ -defmodule ApaewD840 do +defmodule ApaewD840Node0 do require Oracle - @oracle spawn(Oracle, :start, []) - @n "" def n, do: @n @@ -26,8 +24,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] @@ -36,7 +33,7 @@ defmodule ApaewD840 do def send_msg_condition(variables, i) do - Enum.all?([variables[:active][i], Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([i])), fn (j) ->trueend + Enum.all?([variables[:active][i], Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([i])), fn (j) ->true end )]) end @@ -50,9 +47,8 @@ defmodule ApaewD840 do decide_action( List.flatten([ %{ 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(variables)}, true) - , - color: Map.put(variables[:color], {i}, if j(variables) > i, do: "black", else: variables[:color][i]) + active: Map.put(variables[:active], {j(variables)}, true), + color: Map.put(variables[:color], {i}, (if j(variables) > i, do: "black", else: variables[:color][i])) } } ]) ) @@ -60,10 +56,10 @@ defmodule ApaewD840 do end - def main(variables) do + def next(variables) do IO.puts (inspect variables) - main(( + next(( decide_action( List.flatten([ %{ action: "InitiateProbe()", condition: initiate_probe_condition(variables), state: initiate_probe(variables) }, @@ -73,6 +69,16 @@ defmodule ApaewD840 do ) )) end + def main(oracle, variables, step) do + IO.puts(inspect(variables)) + + actions = next(variables) + + next_variables = decide_action(oracle, actions, step) + send(oracle, {:notify, step, variables, next_variables}) + + main(oracle, next_variables, step + 1) + end def decide_action(actions) do possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end) @@ -82,13 +88,14 @@ defmodule ApaewD840 do Enum.count(different_states) == 1 -> Enum.at(possible_actions, 0)[:state] Enum.empty?(different_states) -> - %{} + IO.puts("DEADLOCK") + exit(0) true -> - actions_names = Enum.map(possible_actions, fn(action) -> action[:action] end) - send @oracle, {self(), actions_names} + send oracle, {:choose, self(), possible_actions} n = receive do {:ok, n} -> n + {:stop} -> exit(0) end Enum.at(possible_actions, n)[:state] @@ -96,12 +103,3 @@ defmodule ApaewD840 do end end -ApaewD840.main( - - %{ - active: MapSet.new(nodes_condition(variables), fn(n) -> true end), - color: MapSet.new(nodes_condition(variables), fn(n) -> "white" end), - tpos: 0, - tcolor: "black" - } -) diff --git a/elixir/lib/generated_code/apaew_d840_node1.ex b/elixir/lib/generated_code/apaew_d840_node1.ex index 25d6326..fbcb07f 100644 --- a/elixir/lib/generated_code/apaew_d840_node1.ex +++ b/elixir/lib/generated_code/apaew_d840_node1.ex @@ -1,7 +1,5 @@ -defmodule ApaewD840 do +defmodule ApaewD840Node1 do require Oracle - @oracle spawn(Oracle, :start, []) - @n "" def n, do: @n @@ -13,7 +11,7 @@ defmodule ApaewD840 do def pass_token(variables, i) do %{ tpos: i - 1, - tcolor: if variables[:color][i] == "black", do: "black", else: variables[:tcolor], + tcolor: (if variables[:color][i] == "black", do: "black", else: variables[:tcolor]), active: variables[:active], color: Map.put(variables[:color], {i}, "white") } @@ -26,8 +24,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] @@ -36,7 +33,7 @@ defmodule ApaewD840 do def send_msg_condition(variables, i) do - Enum.all?([variables[:active][i], Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([i])), fn (j) ->trueend + Enum.all?([variables[:active][i], Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([i])), fn (j) ->true end )]) end @@ -50,9 +47,8 @@ defmodule ApaewD840 do decide_action( List.flatten([ %{ 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(variables)}, true) - , - color: Map.put(variables[:color], {i}, if j(variables) > i, do: "black", else: variables[:color][i]) + active: Map.put(variables[:active], {j(variables)}, true), + color: Map.put(variables[:color], {i}, (if j(variables) > i, do: "black", else: variables[:color][i])) } } ]) ) @@ -60,10 +56,10 @@ defmodule ApaewD840 do end - def main(variables) do + def next(variables) do IO.puts (inspect variables) - main(( + next(( decide_action( List.flatten([ %{ action: "PassToken(Lit (Num 1))", condition: pass_token_condition(variables, 1), state: pass_token(variables, 1) }, @@ -73,6 +69,16 @@ defmodule ApaewD840 do ) )) end + def main(oracle, variables, step) do + IO.puts(inspect(variables)) + + actions = next(variables) + + next_variables = decide_action(oracle, actions, step) + send(oracle, {:notify, step, variables, next_variables}) + + main(oracle, next_variables, step + 1) + end def decide_action(actions) do possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end) @@ -82,13 +88,14 @@ defmodule ApaewD840 do Enum.count(different_states) == 1 -> Enum.at(possible_actions, 0)[:state] Enum.empty?(different_states) -> - %{} + IO.puts("DEADLOCK") + exit(0) true -> - actions_names = Enum.map(possible_actions, fn(action) -> action[:action] end) - send @oracle, {self(), actions_names} + send oracle, {:choose, self(), possible_actions} n = receive do {:ok, n} -> n + {:stop} -> exit(0) end Enum.at(possible_actions, n)[:state] @@ -96,12 +103,3 @@ defmodule ApaewD840 do end end -ApaewD840.main( - - %{ - active: MapSet.new(nodes_condition(variables), fn(n) -> true end), - color: MapSet.new(nodes_condition(variables), fn(n) -> "white" end), - tpos: 0, - tcolor: "black" - } -) diff --git a/elixir/lib/generated_code/apaew_d840_node2.ex b/elixir/lib/generated_code/apaew_d840_node2.ex index 4b55325..3202978 100644 --- a/elixir/lib/generated_code/apaew_d840_node2.ex +++ b/elixir/lib/generated_code/apaew_d840_node2.ex @@ -1,7 +1,5 @@ -defmodule ApaewD840 do +defmodule ApaewD840Node2 do require Oracle - @oracle spawn(Oracle, :start, []) - @n "" def n, do: @n @@ -13,7 +11,7 @@ defmodule ApaewD840 do def pass_token(variables, i) do %{ tpos: i - 1, - tcolor: if variables[:color][i] == "black", do: "black", else: variables[:tcolor], + tcolor: (if variables[:color][i] == "black", do: "black", else: variables[:tcolor]), active: variables[:active], color: Map.put(variables[:color], {i}, "white") } @@ -26,8 +24,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] @@ -36,7 +33,7 @@ defmodule ApaewD840 do def send_msg_condition(variables, i) do - Enum.all?([variables[:active][i], Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([i])), fn (j) ->trueend + Enum.all?([variables[:active][i], Enum.any?(MapSet.difference?(nodes_condition(variables), MapSet.new([i])), fn (j) ->true end )]) end @@ -50,9 +47,8 @@ defmodule ApaewD840 do decide_action( List.flatten([ %{ 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(variables)}, true) - , - color: Map.put(variables[:color], {i}, if j(variables) > i, do: "black", else: variables[:color][i]) + active: Map.put(variables[:active], {j(variables)}, true), + color: Map.put(variables[:color], {i}, (if j(variables) > i, do: "black", else: variables[:color][i])) } } ]) ) @@ -60,10 +56,10 @@ defmodule ApaewD840 do end - def main(variables) do + def next(variables) do IO.puts (inspect variables) - main(( + next(( decide_action( List.flatten([ %{ action: "PassToken(Lit (Num 2))", condition: pass_token_condition(variables, 2), state: pass_token(variables, 2) }, @@ -73,6 +69,16 @@ defmodule ApaewD840 do ) )) end + def main(oracle, variables, step) do + IO.puts(inspect(variables)) + + actions = next(variables) + + next_variables = decide_action(oracle, actions, step) + send(oracle, {:notify, step, variables, next_variables}) + + main(oracle, next_variables, step + 1) + end def decide_action(actions) do possible_actions = Enum.filter(actions, fn(action) -> action[:condition] end) @@ -82,13 +88,14 @@ defmodule ApaewD840 do Enum.count(different_states) == 1 -> Enum.at(possible_actions, 0)[:state] Enum.empty?(different_states) -> - %{} + IO.puts("DEADLOCK") + exit(0) true -> - actions_names = Enum.map(possible_actions, fn(action) -> action[:action] end) - send @oracle, {self(), actions_names} + send oracle, {:choose, self(), possible_actions} n = receive do {:ok, n} -> n + {:stop} -> exit(0) end Enum.at(possible_actions, n)[:state] @@ -96,12 +103,3 @@ defmodule ApaewD840 do end end -ApaewD840.main( - - %{ - active: MapSet.new(nodes_condition(variables), fn(n) -> true end), - color: MapSet.new(nodes_condition(variables), fn(n) -> "white" end), - tpos: 0, - tcolor: "black" - } -)