Use config file for blackbox test params

ConfigParser.hs

@@ -14,7 +14,7 @@ jsonFile :: FilePath
 jsonFile = "config-sample.json"
 
 data DistributionConfig =
-  Config [ProcessConfig] [String] [ConstantConfig] String String String String String [BlackboxTest] String
+  Config [ProcessConfig] [String] [ConstantConfig] String String String String String String [BlackboxTest] String
   deriving (Show, Generic)
 
 data ProcessConfig =
@@ -37,12 +37,13 @@ instance FromJSON DistributionConfig where
       cs <- obj .: "constants"
       i <- obj .: "init"
       n <- obj .: "next"
+      m <- obj .: "module_name"
       f <- obj .: "input_format"
       file <- obj .: "input_file"
       g <- obj .: "state_graph"
       bs <- obj .: "blackbox_tests"
       dest <- obj .: "destination_folder"
-      return (Config ps vs cs i n f file g bs dest)
+      return (Config ps vs cs i n m f file g bs dest)
 
 instance FromJSON ProcessConfig where
   parseJSON =
@@ -77,4 +78,4 @@ parseConfig file = do
 -- main = parseJson jsonFile >>= print
 
 processNames :: DistributionConfig -> [String]
-processNames (Config ps _ _ _ _ _ _ _ _ _) = map (\(PConfig n _) -> n) ps
+processNames (Config ps _ _ _ _ _ _ _ _ _ _) = map (\(PConfig n _) -> n) ps

Elixir.hs

@@ -10,7 +10,7 @@ import Helpers
 import Snippets
 
 generate :: Spec -> DistributionConfig -> [(String, ElixirCode)]
-generate (Spec m i n ds) (Config ps shared consts _ _ _ _ _ _ _) =
+generate (Spec m i n ds) (Config ps shared consts _ _ _ _ _ _ _ _) =
   let defs = filter (not . (specialDef i n)) ds
       cs = findConstants ds
       vs = findVariables ds

WitnessTestGeneration.hs

@@ -27,16 +27,22 @@ testFile testTrace modules testName =
     , "end"
     ]
 
-main :: IO ()
+generateTestFromTrace moduleName dest ps (Test n t) = do
+  f <- readFile t
+  case parseTrace f of
+    Right ss ->
+      let content = testFile (map (initialState [] . toValue) ss) (map ((moduleName ++ "_") ++) ps) n
+          outFile = dest ++ "/lib/mix/tasks/" ++ snake n ++ ".ex"
+       in writeFile outFile content
+    Left e -> print e
+
+-- generateBlackboxTests :: [String] -> DistributionConfig -> Either String IO()
+generateBlackboxTests ps (Config _ _ _ _ _ name _ _ _ tests dest) = mapM (generateTestFromTrace name dest ps) tests
+
+-- main :: IO [()]
 main = do
-  (moduleName:file:testName:configFile:_) <- getArgs
-  f <- readFile file
+  (configFile:_) <- getArgs
   config <- parseConfig configFile
-  case fmap processNames config of
-        Left err -> putStrLn err
-        Right ms -> case parseTrace f of
-                      Right ss ->
-                        let content = testFile (map (initialState [] . toValue) ss) (map ((moduleName ++ "_") ++) ms) testName
-                            outFile = "elixir/lib/mix/tasks/" ++ snake testName ++ ".ex"
-                         in writeFile outFile content
-                      Left e -> print e
+  case fmap (\c -> generateBlackboxTests (processNames c) c) config of
+        Left err -> error err
+        Right c -> c

tla_specifications/ERC20/config.json

@@ -38,6 +38,7 @@
   ],
   "init": "Init",
   "next": "Next",
+  "module_name": "ERC20",
   "input_format": "json",
   "input_file": "ERC20.json",
   "state_graph": "states.json",

tla_specifications/ewd840/config.json

@@ -0,0 +1,44 @@
+{
+  "processes": [
+    {
+      "process_id": "node0",
+      "actions": [
+        "InitiateProbe()",
+        "\\E i \\in {1, 2} : SendMsg(0, i)",
+        "Deactivate(0)"
+      ]
+    },
+    {
+      "process_id": "node1",
+      "actions": [
+        "PassToken(1)",
+        "\\E i \\in {0, 2} : SendMsg(1, i)",
+        "Deactivate(1)"
+      ]
+    },
+    {
+      "process_id": "node2",
+      "actions": [
+        "PassToken(2)",
+        "\\E i \\in {0, 1} : SendMsg(2, i)",
+        "Deactivate(2)"
+      ]
+    }
+  ],
+  "shared_variables": ["tcolor", "tpos", "active"],
+  "constants": [
+    {
+      "name": "N",
+      "value": "3"
+    }
+  ],
+  "init": "Init",
+  "next": "Next",
+  "module_name": "APAEWD840",
+  "input_format": "json",
+  "input_file": "APAEWD840.json",
+  "state_graph": "states.json",
+  "blackbox_tests": [{"name": "Termination", "trace": "trace.out"}],
+  "destination_folder": "../../elixir"
+
+}