Generate starter code in a task and isolate stuff

Elixir.hs

@@ -12,30 +12,42 @@ 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
                    in filter (\d -> name d `elem` actionNames) ds
 
 {-- \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 -}

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) ++ ")"

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

Snippets.hs

@@ -10,20 +10,68 @@ 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]",
              "  end",
              "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"
+                             ]