diff --git a/ConfigParser.hs b/ConfigParser.hs index de91116..e65a5d2 100644 --- a/ConfigParser.hs +++ b/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 diff --git a/Elixir.hs b/Elixir.hs index 7afab3d..dbb0ea5 100644 --- a/Elixir.hs +++ b/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 diff --git a/WitnessTestGeneration.hs b/WitnessTestGeneration.hs index e01a8ff..93a8ee9 100644 --- a/WitnessTestGeneration.hs +++ b/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 diff --git a/tla_specifications/ERC20/config.json b/tla_specifications/ERC20/config.json index 11007af..de9719a 100644 --- a/tla_specifications/ERC20/config.json +++ b/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", diff --git a/tla_specifications/ewd840/config.json b/tla_specifications/ewd840/config.json new file mode 100644 index 0000000..9f8b3d8 --- /dev/null +++ b/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" + +} diff --git a/tla_specifications/termination_trace.out b/tla_specifications/ewd840/trace.out similarity index 100% rename from tla_specifications/termination_trace.out rename to tla_specifications/ewd840/trace.out