Organize examples, executables and README

README.md

@@ -1,11 +1,5 @@
 # TLA+ Transmutation
-Elixir code generation from TLA+ specifications
-
-I've started to work on this for my bachelor thesis, which can be found [here](https://github.com/bugarela/bachelor-thesis) (Portuguese only).
-
-The formalization of the translation rules are available at [rules.pdf](rules.pdf)
-
-Notice that this covers only a small portion of TLA+ definitions and it is yet to be incremented with more translations. The Parser itself isn't able to recognize much. Contributions are welcome :D.
+Elixir code and test generation from TLA+ specifications
 
 ## Dependencies
 
@@ -20,27 +14,24 @@ Notice that this covers only a small portion of TLA+ definitions and it is yet t
 [Instructions for installation with asdf package manager](https://elixirgirls.com/install-guides/linux.html)
 
 ## Build
-```sh
-ghc Main.hs
+
+``` sh
+make compile
 ```
 
 ## Run
 
-This currently supports partially 2 forms of parsing:
-1. From `.tla` files: this is deprecated and supports a minimal fragment of the language
-2. From `.json` files produced by [Apalache](https://github.com/informalsystems/apalache)'s parsing: Work in progress.
+The best parsing implementation takes JSON files previously parsed from TLA with [Apalache](https://github.com/informalsystems/apalache):
 
-To generate code, specify the args:
-1. Mode (`tla` or `json`)
-2. Filepath (for the `.tla` or `.json` file)
-3. Init definition name (i.e. `MyInit`)
-4. Next definition name (i.e. `MyNext`)
-
-Some examples:
-```sh
-./Main json tla_specifications/token-transfer/TokenTransfer1.json Init Next
+``` sh
+apalache-mc parse --output=file.json file.tla
 ```
 
+All compliled files (`CodeGenerator`, `WhiteboxTestGenerator` and `BlackboxTestGenerator`) take a single argument which is a JSON-formatted configuration file similar to [config-sample.json](./config-sample.json)
+
+Folders inside [tla_specifications](./tla_specifications) are examples containing the required files for running the three executables. You can `cd` into any of them and run:
+
 ``` sh
-./Main tla tla_specifications/EfetivacaoEmDuasFases.tla DFInit DFNext
+../../CodeGenerator config.json && ../../BlackboxTestGenerator config.json && ../../WhiteboxTestGenerator config.json
 ```
+

StateGraphParser.hs → WhiteboxTestGenerator.hs

@@ -64,7 +64,7 @@ testForNode ms g Node {nodeId = i, label = l} = do
        , "  expectedStates = [" ++ intercalate ",\n" ss ++ "]"
        , ""
        , "  actions = List.flatten([" ++ intercalate ", " (map (++ ".next(variables)") ms) ++ "])"
-       , "  states = Enum.map(actions, fn action -> action[:state] end)"
+       , "  states = Enum.map(actions, fn action -> action[:transition].(variables) end)"
        , ""
        , "  assert Enum.sort(Enum.uniq(states)) == Enum.sort(Enum.uniq(expectedStates))"
        , "end"

config-sample.json

@@ -25,5 +25,19 @@
       ]
     }
   ],
-  "shared_variables": ["tcolor", "tpos", "active"]
+  "shared_variables": ["tcolor", "tpos", "active"],
+  "constants": [
+    {
+      "name": "N",
+      "value": "3"
+    }
+  ],
+  "init": "Init",
+  "next": "Next",
+  "module_name": "EWD840",
+  "input_format": "json",
+  "input_file": "EWD840.json",
+  "state_graph": "states.json",
+  "blackbox_tests": [{"name": "Termination", "trace": "trace.out"}],
+  "destination_folder": "../../elixir"
 }

elixir/lib/generated_code/apaew_d840.ex → elixir/lib/generated_code/ew_d840.ex

@@ -1,4 +1,4 @@
-defmodule APAEWD840 do
+defmodule EWD840 do
   def shared_variables do
     [
       :tcolor,

elixir/lib/generated_code/apaew_d840_node0.ex → elixir/lib/generated_code/ew_d840_node0.ex

@@ -1,7 +1,7 @@
-defmodule APAEWD840_node0 do
+defmodule EWD840_node0 do
   require Oracle
 
-  import APAEWD840
+  import EWD840
 
   def next(variables) do
     Enum.filter(

elixir/lib/generated_code/apaew_d840_node1.ex → elixir/lib/generated_code/ew_d840_node1.ex

@@ -1,7 +1,7 @@
-defmodule APAEWD840_node1 do
+defmodule EWD840_node1 do
   require Oracle
 
-  import APAEWD840
+  import EWD840
 
   def next(variables) do
     Enum.filter(

elixir/lib/generated_code/apaew_d840_node2.ex → elixir/lib/generated_code/ew_d840_node2.ex

@@ -1,7 +1,7 @@
-defmodule APAEWD840_node2 do
+defmodule EWD840_node2 do
   require Oracle
 
-  import APAEWD840
+  import EWD840
 
   def next(variables) do
     Enum.filter(

elixir/lib/generated_code/traffic_semaphores.ex

@@ -6,18 +6,18 @@ defmodule TrafficSemaphores do
     ]
   end
   require Oracle
-  @semaphores "<value for SEMAPHORES>"
+  @semaphores MapSet.new([0, 1])
   def semaphores, do: @semaphores
 
 
   def turn_green_condition(variables, s) do
-    Enum.all?(@semaphores, fn(s2) -> variables[:colors][s2] == "red" end)
+    Enum.all?([Enum.all?(@semaphores, fn(s2) -> variables[:colors][s2] == "red" end), variables[:next_to_open] == s])
   end
 
   def turn_green(variables, s) do
     %{
-      colors: Map.put(variables[:colors], s, "green"),
-      next_to_open: variables[:next_to_open]
+      colors: variables[:colors]|>Map.put(s, "green"),
+      next_to_open: rem((s + 1), (Enum.count(@semaphores)))
     }
   end
 
@@ -28,7 +28,7 @@ defmodule TrafficSemaphores do
 
   def turn_yellow(variables, s) do
     %{
-      colors: Map.put(variables[:colors], s, "yellow"),
+      colors: variables[:colors]|>Map.put(s, "yellow"),
       next_to_open: variables[:next_to_open]
     }
   end
@@ -40,24 +40,25 @@ defmodule TrafficSemaphores do
 
   def turn_red(variables, s) do
     %{
-      colors: Map.put(variables[:colors], s, "red"),
+      colors: variables[:colors]|>Map.put(s, "red"),
       next_to_open: variables[:next_to_open]
     }
   end
 
 
+  # "Spec": OperEx "AND" [OperEx "OPER_APP" [NameEx "Init"],OperEx "GLOBALLY" [OperEx "STUTTER" [OperEx "OPER_APP" [NameEx "Next"],OperEx "TUPLE" [NameEx "colors",NameEx "next_to_open"]]]]
 
   def decide_action(oracle, variables, actions, step) do
-    different_states = Enum.uniq_by(actions, fn(action) -> action[:state] end)
+    different_states = Enum.uniq(Enum.map(actions, fn(action) -> action[:transition].(variables) end))
 
     cond do
       Enum.count(different_states) == 1 ->
-        Enum.at(actions, 0)[:state]
+        Enum.at(different_states, 0)
       true ->
-        send oracle, {:choose, self(), actions}
+        send oracle, {:choose, self(), different_states}
 
        receive do
-         {:ok, n} -> Enum.at(actions, n)[:state]
+         {:ok, n} -> Enum.at(different_states, n)
          {:cancel} -> variables
          {:stop} -> exit(0)
        end

elixir/lib/generated_code/traffic_semaphores_main.ex

@@ -6,10 +6,10 @@ defmodule TrafficSemaphores_main do
   def next(variables) do
     Enum.filter(
       List.flatten([
-      Enum.map(MapSet.new([0, 1]), fn (s) -> [
-        %{ action: "TurnGreen(#{inspect s})", condition: turn_green_condition(variables, s), state: turn_green(variables, s) },
-        %{ action: "TurnYellow(#{inspect s})", condition: turn_yellow_condition(variables, s), state: turn_yellow(variables, s) },
-        %{ action: "TurnRed(#{inspect s})", condition: turn_red_condition(variables, s), state: turn_red(variables, s) }
+      Enum.map(TrafficSemaphores.semaphores, fn (s) -> [
+        %{ action: "TurnGreen(#{inspect s})", condition: turn_green_condition(variables, s), transition: fn (variables) -> turn_green(variables, s) end },
+        %{ action: "TurnYellow(#{inspect s})", condition: turn_yellow_condition(variables, s), transition: fn (variables) -> turn_yellow(variables, s) end },
+        %{ action: "TurnRed(#{inspect s})", condition: turn_red_condition(variables, s), transition: fn (variables) -> turn_red(variables, s) end }
       ] end
       )
     ]),
@@ -21,11 +21,10 @@ defmodule TrafficSemaphores_main 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, variables, actions, step)
-    send(oracle, {:notify, step, variables, next_variables})
+    send(oracle, {:notify, self(), variables, next_variables})
     Process.sleep(2000)
 
     main(oracle, next_variables, step + 1)