diff --git a/CMakeLists.txt b/CMakeLists.txt index c84510a..418a797 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,7 +34,6 @@ find_package(FLEX REQUIRED) add_compile_definitions(DEFAULT_EXPRESSION_VALUE="true") CPMAddPackage(NAME expr VERSION 3.0.6 GITHUB_REPOSITORY sillydan1/expr OPTIONS "ENABLE_Z3 ON") -CPMAddPackage("gh:sillydan1/argvparse@1.2.3") CPMAddPackage("gh:sillydan1/ctl-expr@2.0.4") CPMAddPackage("gh:sillydan1/graphedit-protobuf@1.2.1") @@ -48,6 +47,7 @@ CPMAddPackage("gh:yalibs/yauuid@1.0.2") CPMAddPackage("gh:yalibs/yasetwrappers@1.0.1") CPMAddPackage("gh:yalibs/yapermutation@1.1.3") +CPMAddPackage("gh:bfgroup/lyra#1.6.1") CPMAddPackage("gh:gabime/spdlog@1.14.1") CPMAddPackage("gh:nlohmann/json@3.11.3") CPMAddPackage("gh:neargye/magic_enum@0.9.5") @@ -56,62 +56,79 @@ CPMAddPackage("gh:cpm-cmake/CPMLicenses.cmake@0.0.7") cpm_licenses_create_disclaimer_target(write_licenses "${CMAKE_BINARY_DIR}/third_party.txt" "${CPM_PACKAGES}") add_library(${PROJECT_NAME} SHARED - src/expr-wrappers/interpreter.cpp - src/expr-wrappers/parameterized-expr-evaluator.cpp - src/expr-wrappers/parameterized-ast-factory.cpp - src/ntta/builder/ntta_builder.cpp - src/ntta/tta.cpp - src/ntta/interesting_tocker.cpp - src/plugin_system/plugin_system.cpp - src/verification/forward_reachability.cpp - src/verification/ctl/ctl_sat.cpp - src/util/warnings.cpp - src/util/random.cpp - src/util/string_extensions.cpp) + src/expr-wrappers/interpreter.cpp + src/expr-wrappers/parameterized-expr-evaluator.cpp + src/expr-wrappers/parameterized-ast-factory.cpp + src/ntta/builder/ntta_builder.cpp + src/ntta/tta.cpp + src/ntta/interesting_tocker.cpp + src/plugin_system/plugin_system.cpp + src/verification/forward_reachability.cpp + src/verification/ctl/ctl_sat.cpp + src/util/warnings.cpp + src/util/random.cpp + src/util/string_extensions.cpp) if(${CODE_COVERAGE}) target_link_options(${PROJECT_NAME} PUBLIC --coverage) target_compile_options(${PROJECT_NAME} PUBLIC --coverage) endif() target_link_libraries(${PROJECT_NAME} PUBLIC expr_lang dl pthread ctl_lang graphedit_proto) target_include_directories(${PROJECT_NAME} PUBLIC - ${CMAKE_BINARY_DIR} - ${CMAKE_CURRENT_BINARY_DIR} - ${argvparse_SOURCE_DIR}/include - ${argvparse_SOURCE_DIR}/src - ${rapidjson_SOURCE_DIR}/include - ${ctl-expr_SOURCE_DIR}/include - ${ctl-expr_SOURCE_DIR}/src - ${ctl-expr_SOURCE_DIR}/../ctl-expr-build - ${json_SOURCE_DIR}/include - ${spdlog_SOURCE_DIR}/include - ${expr_SOURCE_DIR}/include - ${expr_SOURCE_DIR}/src - ${expr_BUILD_DIR} - ${optionparser_SOURCE_DIR}/src - ${magic_enum_SOURCE_DIR}/include - ${graphedit-protobuf_BINARY_DIR}/src/main/proto + ${CMAKE_BINARY_DIR} + ${CMAKE_CURRENT_BINARY_DIR} + ${argvparse_SOURCE_DIR}/include + ${argvparse_SOURCE_DIR}/src + ${rapidjson_SOURCE_DIR}/include + ${ctl-expr_SOURCE_DIR}/include + ${ctl-expr_SOURCE_DIR}/src + ${ctl-expr_SOURCE_DIR}/../ctl-expr-build + ${json_SOURCE_DIR}/include + ${spdlog_SOURCE_DIR}/include + ${expr_SOURCE_DIR}/include + ${expr_SOURCE_DIR}/src + ${expr_BUILD_DIR} + ${optionparser_SOURCE_DIR}/src + ${magic_enum_SOURCE_DIR}/include + ${graphedit-protobuf_BINARY_DIR}/src/main/proto - ${yatimer_SOURCE_DIR}/include - ${yaoverload_SOURCE_DIR}/include - ${yahashcombine_SOURCE_DIR}/include - ${yathreadpool_SOURCE_DIR}/include - ${yagraph_SOURCE_DIR}/include - ${yatree_SOURCE_DIR}/include - ${yauuid_SOURCE_DIR}/include - ${yapermutation_SOURCE_DIR}/include - ${yasetwrappers_SOURCE_DIR}/include - src - # strictly not required, but it helps my clangd lsp setup and it doesn't hurt - ${FLEX_INCLUDE_DIRS} - ${BISON_INCLUDE_DIRS} + ${yatimer_SOURCE_DIR}/include + ${yaoverload_SOURCE_DIR}/include + ${yahashcombine_SOURCE_DIR}/include + ${yathreadpool_SOURCE_DIR}/include + ${yagraph_SOURCE_DIR}/include + ${yatree_SOURCE_DIR}/include + ${yauuid_SOURCE_DIR}/include + ${yapermutation_SOURCE_DIR}/include + ${yasetwrappers_SOURCE_DIR}/include + ${lyra_SOURCE_DIR}/include + src + # strictly not required, but it helps my clangd lsp setup and it doesn't hurt + ${FLEX_INCLUDE_DIRS} + ${BISON_INCLUDE_DIRS} ) add_compile_definitions(ENABLE_Z3) -add_subdirectory(src/cli/simulator) -add_subdirectory(src/cli/verifier) -add_subdirectory(src/cli/detcheck) -add_subdirectory(src/cli/lsp) +add_executable(${PROJECT_NAME}-verifier + src/cli/verifier/main.cpp + src/cli/verifier/query/query_json_loader.cpp +) +add_executable(${PROJECT_NAME}-simulator + src/cli/simulator/main.cpp +) +add_executable(${PROJECT_NAME}-detcheck + src/cli/detcheck/main.cpp +) +add_executable(${PROJECT_NAME}-lsp + src/cli/lsp/main.cpp + src/cli/lsp/lsp_server.cpp +) add_subdirectory(src/parser) + +target_link_libraries(${PROJECT_NAME}-verifier ${PROJECT_NAME} ctl argvparse) +target_link_libraries(${PROJECT_NAME}-simulator ${PROJECT_NAME} ctl argvparse) +target_link_libraries(${PROJECT_NAME}-detcheck ${PROJECT_NAME} ctl argvparse) +target_link_libraries(${PROJECT_NAME}-lsp ${PROJECT_NAME} ctl argvparse) + add_subdirectory(test) install(TARGETS ${PROJECT_NAME} expr_lang ctl_lang aaltitoad-verifier aaltitoad-simulator aaltitoad-detcheck aaltitoad-lsp) diff --git a/src/cli/cli_common.h b/src/cli/cli_common.h deleted file mode 100644 index 22fbd82..0000000 --- a/src/cli/cli_common.h +++ /dev/null @@ -1,65 +0,0 @@ -/** - * aaltitoad - a verification engine for tick tock automata models - Copyright (C) 2023 Asger Gitz-Johansen - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . - */ -#ifndef AALTITOAD_CLI_COMMON_H -#define AALTITOAD_CLI_COMMON_H -#include -#include -#include -#include -#include -#include - -inline int print_required_args() { - std::cout << "Required arguments:\n"; - std::cout << " --input / -f\n"; - return 1; -} - -inline int print_help(const std::string& program_name, const std::vector& options) { - std::cout << get_license() << std::endl; - std::cout << PROJECT_NAME << " v" << PROJECT_VER << std::endl; - std::cout << "USAGE: " << program_name << " -f /path/to/tta/dir [OPTIONS] \n" << std::endl; - std::cout << "OPTIONS: " << std::endl; - print_argument_help(options); - return 0; -} - -inline int print_version() { - std::cout << PROJECT_NAME << " v" << PROJECT_VER << std::endl; - return 0; -} - -inline void disable_warnings(const std::vector& disable_warns) { - aaltitoad::warnings::enable_all(); - for(auto& w : disable_warns) { - auto opt = magic_enum::enum_cast(w); - if(opt.has_value()) - aaltitoad::warnings::disable_warning(opt.value()); - else - spdlog::warn("not a warning: {0}", w); - } -} - -inline int list_warnings() { - std::cout << "[WARNINGS]:\n"; - for(const auto& warning : aaltitoad::warnings::descriptions()) - std::cout << "\t - [" << magic_enum::enum_name(warning.first) << "]: " << warning.second << "\n"; - return 0; -} - -#endif //AALTITOAD_CLI_COMMON_H diff --git a/src/cli/detcheck/CMakeLists.txt b/src/cli/detcheck/CMakeLists.txt deleted file mode 100644 index a8b93b9..0000000 --- a/src/cli/detcheck/CMakeLists.txt +++ /dev/null @@ -1,24 +0,0 @@ -# aaltitoad - a verification engine for tick tock automata models -# Copyright (C) 2023 Asger Gitz-Johansen -# -# This program is free software: you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation, either version 3 of the License, or -# (at your option) any later version. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . -# -project(aaltitoad-detcheck VERSION 1.0.0) -find_package(argvparse REQUIRED) -add_executable(${PROJECT_NAME} main.cpp) -target_link_libraries(${PROJECT_NAME} aaltitoad argvparse) -if(TARGET default_plugins) - add_dependencies(${PROJECT_NAME} default_plugins) -endif() -install(TARGETS ${PROJECT_NAME}) diff --git a/src/cli/detcheck/cli_options.h b/src/cli/detcheck/cli_options.h deleted file mode 100644 index 5065442..0000000 --- a/src/cli/detcheck/cli_options.h +++ /dev/null @@ -1,55 +0,0 @@ -/** - * aaltitoad - a verification engine for tick tock automata models - Copyright (C) 2023 Asger Gitz-Johansen - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . - */ -#ifndef AALTITOAD_CLI_OPTIONS_H -#define AALTITOAD_CLI_OPTIONS_H - -std::vector get_options() { - return { - {"input", 'f', argument_requirement::REQUIRE_ARG, "(Required) input folder containing diagram files to parse and simulate"}, - {"version", 'V', argument_requirement::NO_ARG, "Print version and exit"}, - {"verbosity", 'v', argument_requirement::REQUIRE_ARG, "Set verbosity level (6 for max verbosity)"}, - {"ignore", 'i', argument_requirement::REQUIRE_ARG, "Specify a file to ignore (-i file1 -i file2 for multiple files)"}, - {"parser", 'p', argument_requirement::REQUIRE_ARG, "Specify the parser to use"}, - {"plugin-dir", 'P', argument_requirement::REQUIRE_ARG, "Specify directories to look for parser plugins"}, - {"instance", 'n', argument_requirement::REQUIRE_ARG, "Specify tta instances to check"}, - {"instance-file", 'N', argument_requirement::REQUIRE_ARG, "Specify a json-encoded file containing tta instances to check"}, - {"list-instances",'L', argument_requirement::NO_ARG, "List available instances and exit"}, - - {"known", 'k', argument_requirement::REQUIRE_ARG, "Specify known symbol declarations"}, - {"known-file", 'K', argument_requirement::REQUIRE_ARG, "Specify a json-encoded file containing known symbol declarations"}, - {"condition", 'c', argument_requirement::REQUIRE_ARG, "Specify a condition. This will be added to all bool checks"}, - {"condition-file",'C', argument_requirement::REQUIRE_ARG, "Specify a json-encoded file containing extra conditions"}, - }; -} - -bool is_required(const std::string& s) { - if(s == "input") - return true; - return false; -} - -bool is_required_provided(std::map& provided_args, const std::vector& options) { - if(provided_args["version"]) - return true; - for(auto& opt : options) { - if(is_required(opt.long_option) && !provided_args[opt.long_option]) - return false; - } - return true; -} -#endif //AALTITOAD_CLI_OPTIONS_H diff --git a/src/cli/detcheck/main.cpp b/src/cli/detcheck/main.cpp index 342d569..0ef67df 100644 --- a/src/cli/detcheck/main.cpp +++ b/src/cli/detcheck/main.cpp @@ -15,60 +15,112 @@ You should have received a copy of the GNU General Public License along with this program. If not, see . */ -#include "cli/simulator/cli_options.h" #include "expr-wrappers/interpreter.h" +#include "util/warnings.h" #include -#include +#include +#include #include #include #include -auto get_ntta(std::map& cli_arguments) -> std::unique_ptr; -auto load_plugins(std::map& cli_arguments) -> plugin_map_t; -void find_deadlocks(const std::unique_ptr& ntta, std::map& cli_arguments); +auto get_ntta(const std::vector& plugin_dirs, const std::vector& ignore_list, const std::string& parser, const std::vector& input) -> std::unique_ptr; +void find_deadlocks(const std::unique_ptr& ntta, const std::vector& conditions, const std::optional& condition_file, const std::vector knowns, const std::optional& known_file, const std::vector& instance, const std::optional& instance_file); int main(int argc, char** argv) { - auto options = get_options(); - auto cli_arguments = get_arguments(options, argc, argv); - if(cli_arguments["verbosity"]) - spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - cli_arguments["verbosity"].as_integer())); - if(cli_arguments["version"]) - return print_version(); - if(cli_arguments["help"]) - return print_help(argv[0], options); - if(!is_required_provided(cli_arguments, options)) - return print_required_args(); - - spdlog::trace("welcome to {0} v{1}", PROJECT_NAME, PROJECT_VER); - auto automata = get_ntta(cli_arguments); - if(cli_arguments["list-instances"]) { + bool show_help = false; + std::vector input = {}; + int verbosity = SPDLOG_LEVEL_INFO; + bool show_version = false; + std::vector ignore = {}; + std::vector plugin_dirs = {}; + bool list_plugins = false; + std::string parser = "huppaal_parser"; + std::vector instances = {}; + std::optional instance_file = {}; + bool list_instances = false; + std::vector known_declarations = {}; + std::optional known_file = {}; + std::vector condition = {}; + std::optional condition_file = {}; + auto cli = lyra::cli() + | lyra::help(show_help).description("Tool to check for non-determinism in a NTTA") + ("show this message") + | lyra::opt(input, "DIR") + ["-f"]["--input"]("add input directory to parse and simulate").required() + | lyra::opt(verbosity, "0-6") + ["-v"]["--verbosity"]("set verbosity level, default: " + std::to_string(verbosity)) + | lyra::opt(show_version) + ["-V"]["--version"]("show version") + | lyra::opt(ignore, "GLOB") + ["-i"]["--ignore"]("add a glob file pattern to ignore") + | lyra::opt(plugin_dirs, "DIR") + ["-d"]["--plugin-dir"]("use a directory to look for plugins") + | lyra::opt(list_plugins) + ["-L"]["--list-plugins"]("list found plugins and exit") + | lyra::opt(parser, "PARSER") + ["-p"]["--parser"]("the parser to use") + | lyra::opt(instances, "INSTANCE") + ["-n"]["--instance"]("add a TTA instance to check") + | lyra::opt(instance_file, "FILE") + ["-N"]["--instance-file"]("set a json file with TTA instances to check") + | lyra::opt(list_instances) + ["-L"]["--list-instances"]("list available instances and exit") + | lyra::opt(known_declarations, "EXPR") + ["-k"]["--known"]("set known symbols declaration expression") + | lyra::opt(known_file, "FILE") + ["-K"]["--known-file"]("set a json file with known symbol declarations") + | lyra::opt(condition, "EXPR") + ["-c"]["--condition"]("set the condition to check") + | lyra::opt(condition_file, "FILE") + ["-C"]["--condition-file"]("set a json file with conditions to check") + ; + auto args = cli.parse({argc, argv}); + if(show_help) { + std::cout << cli << std::endl; + return 0; + } + if(verbosity < 0 || verbosity > SPDLOG_LEVEL_OFF) { + std::cout << "verbosity must be within 0-6" << std::endl; + return 1; + } + spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - verbosity)); + spdlog::trace("welcome to {} v{}", PROJECT_NAME, PROJECT_VER); + if(show_version) { + std::cout << PROJECT_NAME << " v" << PROJECT_VER << std::endl; + return 0; + } + if(!args) { + spdlog::error(args.message()); + return 1; + } + + auto automata = get_ntta(plugin_dirs, ignore, parser, input); + if(list_instances) { for(auto& c: automata->components) std::cout << c.first << " "; std::cout << std::endl; - } else { - find_deadlocks(automata, cli_arguments); + return 0; } - std::cout << "done" << std::endl; + + spdlog::trace("looking for deadlocks"); + find_deadlocks(automata, condition, condition_file, known_declarations, known_file, instances, instance_file); return 0; } -auto get_ntta(std::map& cli_arguments) -> std::unique_ptr { +auto get_ntta(const std::vector& plugin_dirs, const std::vector& ignore_list, const std::string& parser, const std::vector& input) -> std::unique_ptr { /// Load plugins - auto available_plugins = load_plugins(cli_arguments); - - /// Parser related arguments - auto ignore_list = cli_arguments["ignore"].as_list_or_default({}); + auto available_plugins = aaltitoad::plugins::load(plugin_dirs); /// Get the parser - auto selected_parser = cli_arguments["parser"].as_string_or_default("huppaal_parser"); - if(!available_plugins.contains(selected_parser) || available_plugins.at(selected_parser).type != plugin_type::parser) - throw std::logic_error("no such parser available: " + selected_parser); + if(!available_plugins.contains(parser) || available_plugins.at(parser).type != plugin_type::parser) + throw std::logic_error("no such parser available: " + parser); /// Parse provided model - spdlog::trace("parsing with {0} plugin", selected_parser); - auto parser = std::get(available_plugins.at(selected_parser).function)(); + spdlog::trace("parsing with {0} plugin", parser); + auto p = std::get(available_plugins.at(parser).function)(); ya::timer t{}; - auto parse_result = parser->parse_files(cli_arguments["input"].as_list(), ignore_list); + auto parse_result = p->parse_files(input, ignore_list); for(auto& diagnostic : parse_result.diagnostics) aaltitoad::warnings::print_diagnostic(diagnostic); if(!parse_result.result.has_value()) @@ -78,16 +130,6 @@ auto get_ntta(std::map& cli_arguments) -> std::unique_p return automata; } -auto load_plugins(std::map& cli_arguments) -> plugin_map_t { - auto rpath = std::getenv("AALTITOAD_LIBPATH"); - std::vector look_dirs = { ".", "lib", "plugins" }; - if(rpath) - look_dirs.emplace_back(rpath); - auto provided_dirs = cli_arguments["plugin-dir"].as_list_or_default({}); - look_dirs.insert(look_dirs.end(), provided_dirs.begin(), provided_dirs.end()); - return aaltitoad::plugins::load(look_dirs); -} - auto get_mentioned_symbols(const expr::syntax_tree_t& expression, const expr::symbol_table_t& symbols) -> expr::symbol_table_t { expr::symbol_table_t mentioned{}; std::visit(ya::overload( @@ -108,19 +150,19 @@ auto get_mentioned_symbols(const expr::syntax_tree_t& expression, const expr::sy return mentioned; } -void find_deadlocks(const std::unique_ptr& ntta, std::map& cli_arguments) { +void find_deadlocks(const std::unique_ptr& ntta, const std::vector& conditions, const std::optional& condition_file, const std::vector knowns, const std::optional& known_file, const std::vector& instance, const std::optional& instance_file) { ya::timer t{}; aaltitoad::expression_driver c{ntta->symbols, ntta->external_symbols}; std::vector extra_conditions{}; - for(auto& condition : cli_arguments["condition"].as_list_or_default({})) { + for(auto& condition : conditions) { auto result = c.parse(condition); if(!result.expression) spdlog::error("only raw expressions will be used for extra conditions"); else extra_conditions.push_back(result.expression.value()); } - if(cli_arguments["condition-file"]) { - std::ifstream f(cli_arguments["condition-file"].as_string()); + if(condition_file.has_value()) { + std::ifstream f(condition_file.value()); nlohmann::json data = nlohmann::json::parse(f); for(auto& condition : data["conditions"]) { auto result = c.parse(condition); @@ -134,10 +176,10 @@ void find_deadlocks(const std::unique_ptr& ntta, std::map& ntta, std::map. -# -project(aaltitoad-lsp VERSION 1.0.0) -find_package(argvparse REQUIRED) -add_executable(${PROJECT_NAME} main.cpp lsp_server.cpp) -target_link_libraries(${PROJECT_NAME} aaltitoad argvparse) -target_include_directories(${PROJECT_NAME} PUBLIC - ${graphedit-protobuf_BINARY_DIR}/src/main/proto -) -if(TARGET default_plugins) - add_dependencies(${PROJECT_NAME} default_plugins) -endif() -install(TARGETS ${PROJECT_NAME}) diff --git a/src/cli/lsp/cli_options.h b/src/cli/lsp/cli_options.h deleted file mode 100644 index dab4d47..0000000 --- a/src/cli/lsp/cli_options.h +++ /dev/null @@ -1,45 +0,0 @@ -/** - * aaltitoad - a verification engine for tick tock automata models - Copyright (C) 2023 Asger Gitz-Johansen - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . - */ -#ifndef AALTITOAD_CLI_OPTIONS_H -#define AALTITOAD_CLI_OPTIONS_H -#include "arguments.h" - -inline std::vector get_options() { - return { - {"version", 'V', argument_requirement::NO_ARG, "Print version and exit"}, - {"verbosity", 'v', argument_requirement::REQUIRE_ARG, "Set verbosity level (6 for max verbosity)"}, - {"port", 'p', argument_requirement::REQUIRE_ARG, "Set language server port (default 5001)"}, - {"list-plugins",'L', argument_requirement::NO_ARG, "List found plugins and exit"}, - {"parser", 'P', argument_requirement::REQUIRE_ARG, "Specify the parser to use"}, - }; -} - -inline bool is_required(const std::string& s) { - return false; -} - -inline bool is_required_provided(std::map& provided_args, const std::vector& options) { - if(provided_args["version"]) - return true; - for(auto& opt : options) - if(is_required(opt.long_option) && !provided_args[opt.long_option]) - return false; - return true; -} - -#endif //AALTITOAD_CLI_OPTIONS_H diff --git a/src/cli/lsp/main.cpp b/src/cli/lsp/main.cpp index be9c712..e27022a 100644 --- a/src/cli/lsp/main.cpp +++ b/src/cli/lsp/main.cpp @@ -15,17 +15,15 @@ You should have received a copy of the GNU General Public License along with this program. If not, see . */ -#include "cli_options.h" #include "lsp_server.h" #include -#include +#include #include +#include #include #include #include -auto load_plugins(std::map& cli_arguments) -> plugin_map_t; - void siginthandler(int param) { spdlog::info("exiting ({})", param); exit(param); @@ -33,52 +31,68 @@ void siginthandler(int param) { int main(int argc, char** argv) { signal(SIGINT, siginthandler); - auto options = get_options(); - // TODO: add option to control grpc verbosity: gpr_set_log_verbosity(gpr_log_severity::GPR_LOG_SEVERITY_DEBUG); - auto cli_arguments = get_arguments(options, argc, argv); - if(cli_arguments["verbosity"]) - spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - cli_arguments["verbosity"].as_integer())); - if(cli_arguments["version"]) - return print_version(); - if(cli_arguments["help"]) - return print_help(argv[0], options); - if(!is_required_provided(cli_arguments, options)) - return print_required_args(); - + bool show_help = false; + int verbosity = SPDLOG_LEVEL_INFO; + bool show_version = false; + std::vector plugin_dirs = {}; + std::string parser = "huppaal_parser"; + bool list_plugins = false; + int port = 5001; + auto cli = lyra::cli() + | lyra::help(show_help).description("A MLSP (Model Language Server Protocol) server implementation") + ("show this message") + | lyra::opt(verbosity, "0-6") + ["-v"]["--verbosity"]("set verbosity level, default: " + std::to_string(verbosity)) + | lyra::opt(show_version) + ["-V"]["--version"]("show version") + | lyra::opt(plugin_dirs, "DIR") + ["-d"]["--plugin-dir"]("use a directory to look for plugins") + | lyra::opt(parser, "PARSER") + ["-p"]["--parser"]("set a parser to use, default: " + parser) + | lyra::opt(list_plugins) + ["-L"]["--list-plugins"]("list found plugins and exit") + | lyra::opt(port, "PORT") + ["-P"]["--port"]("set port to host the lsp, default: " + std::to_string(port)) + ; + auto args = cli.parse({argc, argv}); + if(show_help) { + std::cout << cli << std::endl; + return 0; + } + if(verbosity < 0 || verbosity > SPDLOG_LEVEL_OFF) { + std::cout << "verbosity must be within 0-6" << std::endl; + return 1; + } + spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - verbosity)); spdlog::trace("welcome to {} v{}", PROJECT_NAME, PROJECT_VER); + if(show_version) { + std::cout << PROJECT_NAME << " v" << PROJECT_VER << std::endl; + return 0; + } + if(!args) { + spdlog::error(args.message()); + return 1; + } - /// Load plugins - auto available_plugins = load_plugins(cli_arguments); - if(cli_arguments["list-plugins"]) { + spdlog::trace("loading plugins"); + auto available_plugins = aaltitoad::plugins::load(plugin_dirs); + if(list_plugins) { std::cout << "available plugins:\n" << available_plugins; return 0; } - /// Get the parser - auto selected_parser = cli_arguments["parser"].as_string_or_default("huppaal_parser"); - if(!available_plugins.contains(selected_parser) || available_plugins.at(selected_parser).type != plugin_type::parser) { - spdlog::error("no such parser available: '{0}'", selected_parser); + spdlog::trace("loading parser"); + if(!available_plugins.contains(parser) || available_plugins.at(parser).type != plugin_type::parser) { + spdlog::error("no such parser available: '{}'", parser); return 1; } - spdlog::trace("building parser {}", selected_parser); - std::shared_ptr parser{std::get(available_plugins.at(selected_parser).function)()}; + spdlog::trace("building parser {}", parser); + std::shared_ptr p{std::get(available_plugins.at(parser).function)()}; + spdlog::trace("starting language server..."); - aaltitoad::lsp::proto::LanguageServerImpl{ - cli_arguments["port"].as_integer_or_default(5001), - PROJECT_VER, - parser - }.start(); + aaltitoad::lsp::proto::LanguageServerImpl{port, PROJECT_VER, p}.start(); + spdlog::trace("shutting down {} v{}", PROJECT_NAME, PROJECT_VER); return 0; } - -auto load_plugins(std::map& cli_arguments) -> plugin_map_t { - auto rpath = std::getenv("AALTITOAD_LIBPATH"); - std::vector look_dirs = { ".", "lib", "plugins" }; - if(rpath) - look_dirs.emplace_back(rpath); - auto provided_dirs = cli_arguments["plugin-dir"].as_list_or_default({}); - look_dirs.insert(look_dirs.end(), provided_dirs.begin(), provided_dirs.end()); - return aaltitoad::plugins::load(look_dirs); -} diff --git a/src/cli/simulator/CMakeLists.txt b/src/cli/simulator/CMakeLists.txt deleted file mode 100644 index c27a08c..0000000 --- a/src/cli/simulator/CMakeLists.txt +++ /dev/null @@ -1,25 +0,0 @@ -# aaltitoad - a verification engine for tick tock automata models -# Copyright (C) 2023 Asger Gitz-Johansen -# -# This program is free software: you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation, either version 3 of the License, or -# (at your option) any later version. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . -# -project(aaltitoad-simulator VERSION 1.0.0) -find_package(argvparse REQUIRED) -add_executable(${PROJECT_NAME} main.cpp) -target_link_libraries(${PROJECT_NAME} aaltitoad argvparse) -if(TARGET default_plugins) - add_dependencies(${PROJECT_NAME} default_plugins) -endif() -install(TARGETS ${PROJECT_NAME}) -#install(FILES man/simulator.1 DESTINATION /man/man1) diff --git a/src/cli/simulator/cli_options.h b/src/cli/simulator/cli_options.h deleted file mode 100644 index 1356a85..0000000 --- a/src/cli/simulator/cli_options.h +++ /dev/null @@ -1,61 +0,0 @@ -/** - * aaltitoad - a verification engine for tick tock automata models - Copyright (C) 2023 Asger Gitz-Johansen - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . - */ -#ifndef AALTITOAD_CLI_OPTIONS_H -#define AALTITOAD_CLI_OPTIONS_H -#include -#include -#include - -std::vector get_options() { - return { - {"input", 'f', argument_requirement::REQUIRE_ARG, "(Required) input folder containing diagram files to parse and simulate"}, - {"version", 'V', argument_requirement::NO_ARG, "Print version and exit"}, - {"verbosity", 'v', argument_requirement::REQUIRE_ARG, "Set verbosity level (6 for max verbosity)"}, - {"ignore", 'i', argument_requirement::REQUIRE_ARG, "Specify a file to ignore (-i file1 -i file2 for multiple files)"}, - - {"tocker", 't', argument_requirement::REQUIRE_ARG, "Specify a tocker by name to instantiate"}, - {"parser", 'p', argument_requirement::REQUIRE_ARG, "Specify the parser to use"}, - - {"plugin-dir", 'P', argument_requirement::REQUIRE_ARG, "Specify directories to look for parser plugins"}, - {"list-plugins",'L', argument_requirement::NO_ARG, "List found plugins and exit"}, - - {"ticks", 'n', argument_requirement::REQUIRE_ARG, "Specify the amount of ticks to perform default is infinite"}, - - {"disable-warn",'w', argument_requirement::REQUIRE_ARG, "Disable a warning"}, - {"list-warn", 'W', argument_requirement::NO_ARG, "List all warnings available"}, - {"no-warn", 'm', argument_requirement::NO_ARG, "Disable all warnings"}, - }; -} - -bool is_required(const std::string& s) { - if(s == "input") - return true; - return false; -} - -bool is_required_provided(std::map& provided_args, const std::vector& options) { - if(provided_args["version"]) - return true; - for(auto& opt : options) { - if(is_required(opt.long_option) && !provided_args[opt.long_option]) - return false; - } - return true; -} - -#endif diff --git a/src/cli/simulator/main.cpp b/src/cli/simulator/main.cpp index 41ff82a..6f65872 100644 --- a/src/cli/simulator/main.cpp +++ b/src/cli/simulator/main.cpp @@ -15,75 +15,118 @@ You should have received a copy of the GNU General Public License along with this program. If not, see . */ -#include "../cli_common.h" -#include "cli_options.h" #include "util/warnings.h" #include #include +#include +#include #include #include #include -void parse_and_execute_simulator(std::map& cli_arguments); -auto load_plugins(std::map& cli_arguments) -> plugin_map_t; auto instantiate_tocker(const std::string& arg, const plugin_map_t& available_plugins, const aaltitoad::ntta_t& automata) -> std::optional>; +void disable_warnings(const std::vector& disable_warns); int main(int argc, char** argv) { - auto options = get_options(); - auto cli_arguments = get_arguments(options, argc, argv); - if(cli_arguments["verbosity"]) - spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - cli_arguments["verbosity"].as_integer())); - if(cli_arguments["version"]) - return print_version(); - if(cli_arguments["list-warn"]) - return list_warnings(); - if(cli_arguments["help"]) - return print_help(argv[0], options); - if(!is_required_provided(cli_arguments, options)) - return print_required_args(); - if(cli_arguments["no-warn"]) + bool show_help = false; + int verbosity = SPDLOG_LEVEL_INFO; + bool show_version = false; + std::vector input = {}; + std::vector plugin_dirs = {}; + std::string parser = "huppaal_parser"; + bool list_plugins = false; + std::vector ignore = {}; + std::vector tockers = {}; + int ticks = -1; + std::vector disabled_warnings = {}; + bool list_warnings = false; + bool no_warnings = false; + auto cli = lyra::cli() + | lyra::help(show_help).description("NTTA simulator / runtime with possibility of extensions through tockers") + ("show this message") + | lyra::opt(verbosity, "0-6") + ["-v"]["--verbosity"]("set verbosity level, default: " + std::to_string(verbosity)) + | lyra::opt(show_version) + ["-V"]["--version"]("show version") + | lyra::opt(input, "DIR") + ["-f"]["--input"]("add input directory to parse and simulate").required() + | lyra::opt(plugin_dirs, "DIR") + ["-d"]["--plugin-dir"]("use a directory to look for plugins") + | lyra::opt(parser, "PARSER") + ["-p"]["--parser"]("set a parser to use, default: " + parser) + | lyra::opt(list_plugins) + ["-L"]["--list-plugins"]("list found plugins and exit") + | lyra::opt(ignore, "GLOB") + ["-i"]["--ignore"]("add a glob file pattern to ignore") + | lyra::opt(tockers, "TOCKER") + ["-t"]["--tocker"]("add a tocker to instantiate") + | lyra::opt(ticks, "NUM") + ["-n"]["--ticks"]("set amount of ticks to run, default: " + std::to_string(ticks)) + | lyra::opt(disabled_warnings, "WARN") + ["-w"]["--disable-warning"]("disable a warning") + | lyra::opt(list_warnings) + ["-W"]["--list-warnings"]("list all available warnings and exit") + | lyra::opt(no_warnings) + ["-m"]["--no-warnings"]("disable all warnings") + ; + auto args = cli.parse({argc, argv}); + if(show_help) { + std::cout << cli << std::endl; + return 0; + } + if(verbosity < 0 || verbosity > SPDLOG_LEVEL_OFF) { + std::cout << "verbosity must be within 0-6" << std::endl; + return 1; + } + spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - verbosity)); + spdlog::trace("welcome to {} v{}", PROJECT_NAME, PROJECT_VER); + if(show_version) { + std::cout << PROJECT_NAME << " v" << PROJECT_VER << std::endl; + return 0; + } + if(!args) { + spdlog::error(args.message()); + return 1; + } + if(list_warnings) { + std::cout << "[WARNINGS]:\n"; + for(const auto& warning : aaltitoad::warnings::descriptions()) + std::cout << "\t - [" << magic_enum::enum_name(warning.first) << "]: " << warning.second << "\n"; + return 0; + } + if(no_warnings) aaltitoad::warnings::disable_all(); - disable_warnings(cli_arguments["disable-warn"].as_list_or_default({})); - - spdlog::trace("welcome to {0} v{1}", PROJECT_NAME, PROJECT_VER); - parse_and_execute_simulator(cli_arguments); - return 0; -} + disable_warnings(disabled_warnings); -void parse_and_execute_simulator(std::map& cli_arguments) { /// Load plugins - auto available_plugins = load_plugins(cli_arguments); - if(cli_arguments["list-plugins"]) { + auto available_plugins = aaltitoad::plugins::load(plugin_dirs); + if(list_plugins) { std::cout << "available plugins:\n" << available_plugins; - return; + return 0; } - /// Parser related arguments - auto ignore_list = cli_arguments["ignore"].as_list_or_default({}); - /// Get the parser - auto selected_parser = cli_arguments["parser"].as_string_or_default("huppaal_parser"); - if(!available_plugins.contains(selected_parser) || available_plugins.at(selected_parser).type != plugin_type::parser) { - spdlog::error("no such parser available: '{0}'", selected_parser); - return; + if(!available_plugins.contains(parser) || available_plugins.at(parser).type != plugin_type::parser) { + spdlog::error("no such parser available: '{0}'", parser); + return 1; } /// Parse provided model - spdlog::trace("parsing with {0} plugin", selected_parser); - auto parser = std::get(available_plugins.at(selected_parser).function)(); + spdlog::trace("parsing with {0} plugin", parser); + auto p = std::get(available_plugins.at(parser).function)(); ya::timer t{}; - auto parse_result = parser->parse_files(cli_arguments["input"].as_list(), ignore_list); + auto parse_result = p->parse_files(input, ignore); spdlog::trace("model parsing took {0}ms", t.milliseconds_elapsed()); for(auto& diagnostic : parse_result.diagnostics) aaltitoad::warnings::print_diagnostic(diagnostic); if(!parse_result.result.has_value()) { spdlog::error("compilation failed"); - return; + return 1; } auto automata = std::move(parse_result.result.value()); /// Inject tockers - CLI Format: "name(argument)" - for(auto& arg : cli_arguments["tocker"].as_list_or_default({})) { + for(auto& arg : tockers) { auto tocker = instantiate_tocker(arg, available_plugins, *automata); if(tocker.has_value()) automata->tockers.emplace_back(std::move(tocker.value())); @@ -91,13 +134,12 @@ void parse_and_execute_simulator(std::map& cli_argument /// Run t.start(); - auto maxTicks = cli_arguments["ticks"].as_integer_or_default(-1); spdlog::trace("simulating..."); unsigned int i = 0; #ifdef NDEBUG try { #endif - for (; i < maxTicks || maxTicks < 0; i++) { + for (; i < ticks || ticks < 0; i++) { if(spdlog::get_level() <= spdlog::level::trace) { std::stringstream ss{}; ss << "state:\n" << *automata; @@ -118,16 +160,6 @@ void parse_and_execute_simulator(std::map& cli_argument spdlog::trace("{0} ticks took {1}ms", i, t.milliseconds_elapsed()); } -auto load_plugins(std::map& cli_arguments) -> plugin_map_t { - auto rpath = std::getenv("AALTITOAD_LIBPATH"); - std::vector look_dirs = { ".", "lib", "plugins" }; - if(rpath) - look_dirs.emplace_back(rpath); - auto provided_dirs = cli_arguments["plugin-dir"].as_list_or_default({}); - look_dirs.insert(look_dirs.end(), provided_dirs.begin(), provided_dirs.end()); - return aaltitoad::plugins::load(look_dirs); -} - auto instantiate_tocker(const std::string& arg, const plugin_map_t& available_plugins, const aaltitoad::ntta_t& automata) -> std::optional> { try { auto s = split(arg, "("); @@ -150,3 +182,14 @@ auto instantiate_tocker(const std::string& arg, const plugin_map_t& available_pl return {}; } } + +void disable_warnings(const std::vector& disable_warns) { + aaltitoad::warnings::enable_all(); + for(auto& w : disable_warns) { + auto opt = magic_enum::enum_cast(w); + if(opt.has_value()) + aaltitoad::warnings::disable_warning(opt.value()); + else + spdlog::warn("not a warning: {0}", w); + } +} diff --git a/src/cli/verifier/CMakeLists.txt b/src/cli/verifier/CMakeLists.txt deleted file mode 100644 index ead24a7..0000000 --- a/src/cli/verifier/CMakeLists.txt +++ /dev/null @@ -1,24 +0,0 @@ -# aaltitoad - a verification engine for tick tock automata models -# Copyright (C) 2023 Asger Gitz-Johansen -# -# This program is free software: you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation, either version 3 of the License, or -# (at your option) any later version. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . -# -project(aaltitoad-verifier VERSION 1.1.0) -find_package(argvparse REQUIRED) -add_executable(${PROJECT_NAME} main.cpp query/query_json_loader.cpp) -target_link_libraries(${PROJECT_NAME} aaltitoad ctl argvparse) -if(TARGET default_plugins) - add_dependencies(${PROJECT_NAME} default_plugins) -endif() -install(TARGETS ${PROJECT_NAME}) diff --git a/src/cli/verifier/cli_options.h b/src/cli/verifier/cli_options.h deleted file mode 100644 index a03fa8d..0000000 --- a/src/cli/verifier/cli_options.h +++ /dev/null @@ -1,72 +0,0 @@ -/** - * aaltitoad - a verification engine for tick tock automata models - Copyright (C) 2023 Asger Gitz-Johansen - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . - */ -#ifndef AALTITOAD_CLI_OPTIONS_H -#define AALTITOAD_CLI_OPTIONS_H -#include "arguments.h" -#include -#include -#include -#include -#include - -std::vector get_options() { - return { - {"input", 'f', argument_requirement::REQUIRE_ARG, "(Required) input folder containing diagram files"}, - {"version", 'V', argument_requirement::NO_ARG, "Print version and exit"}, - {"verbosity", 'v', argument_requirement::REQUIRE_ARG, "Set verbosity level (6 for max verbosity)"}, - {"ignore", 'i', argument_requirement::REQUIRE_ARG, "GNU-style regex for filename(s) to ignore"}, - - {"parser", 'p', argument_requirement::REQUIRE_ARG, "Which parser to use"}, - {"query-file", 'q', argument_requirement::REQUIRE_ARG, "Query definition json file"}, - {"query", 'Q', argument_requirement::REQUIRE_ARG, "Add a CTL query to verify"}, - - {"pick-strategy", 's', argument_requirement::REQUIRE_ARG, "Waiting list pick strategy [first|last|random]. Default is first"}, - - {"plugin-dir", 'P', argument_requirement::REQUIRE_ARG, "Directories to look for parser plugins"}, - {"list-plugins", 'L', argument_requirement::NO_ARG, "List found plugins and exit"}, - - {"disable-warn", 'w', argument_requirement::REQUIRE_ARG, "Disable a warning"}, - {"list-warn", 'W', argument_requirement::NO_ARG, "List all warnings available"}, - {"no-warn", 'm', argument_requirement::NO_ARG, "Disable all warnings"}, - - {"result-file", 't', argument_requirement::REQUIRE_ARG, "Provide file to output results to. Default is stdout"}, - {"result-json", 'j', argument_requirement::NO_ARG, "Output results as json. Useful for scripting"}, - }; -} - -bool is_required(const std::string& s) { - if(s == "input") - return true; - return false; -} - -bool is_required_provided(std::map& provided_args, const std::vector& options) { - if(provided_args["version"]) - return true; - if(!provided_args["query-file"] && !provided_args["query"]) { - spdlog::critical("must provide either at least one query with '--query-file' or '--query'"); - return false; - } - for(auto& opt : options) { - if(is_required(opt.long_option) && !provided_args[opt.long_option]) - return false; - } - return true; -} - -#endif //AALTITOAD_CLI_OPTIONS_H diff --git a/src/cli/verifier/main.cpp b/src/cli/verifier/main.cpp index 48d2c90..9d241e0 100644 --- a/src/cli/verifier/main.cpp +++ b/src/cli/verifier/main.cpp @@ -15,71 +15,131 @@ You should have received a copy of the GNU General Public License along with this program. If not, see . */ +#include "expr-wrappers/ctl-interpreter.h" +#include "query/query_json_loader.h" +#include "spdlog/common.h" +#include "spdlog/spdlog.h" +#include "verification/pick_strategy.h" #include +#include #include +#include +#include #include +#include +#include +#include #include -#include #include +#include #include -#include -#include "cli_options.h" -#include "../cli_common.h" -#include -#include -#include "expr-wrappers/ctl-interpreter.h" -#include -#include "query/query_json_loader.h" -#include "spdlog/common.h" -#include "spdlog/spdlog.h" -#include "verification/pick_strategy.h" -auto load_plugins(std::map& cli_arguments) -> plugin_map_t; void trace_log_ntta(const aaltitoad::ntta_t& n); +void disable_warnings(const std::vector& disable_warns); int main(int argc, char** argv) { try { - auto options = get_options(); - auto cli_arguments = get_arguments(options, argc, argv); - if(cli_arguments["verbosity"]) - spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - cli_arguments["verbosity"].as_integer())); - if(cli_arguments["version"]) - return print_version(); - if(cli_arguments["list-warn"]) - return list_warnings(); - if(cli_arguments["help"]) - return print_help(argv[0], options); - if(!is_required_provided(cli_arguments, options)) - return print_required_args(); - spdlog::trace("welcome to {0} v{1}", PROJECT_NAME, PROJECT_VER); - if(cli_arguments["no-warn"]) + bool show_help = false; + int verbosity = SPDLOG_LEVEL_INFO; + bool show_version = false; + std::vector input = {}; + std::vector plugin_dirs = {}; + std::string parser = "huppaal_parser"; + bool list_plugins = false; + std::vector ignore = {}; + std::vector query = {}; + std::vector query_files = {}; + std::string pick_strategy = "first"; + std::vector disabled_warnings = {}; + bool list_warnings = false; + bool no_warnings = false; + std::optional result_file = {}; + bool output_json = false; + auto cli = lyra::cli() + | lyra::help(show_help).description("An extendable verifier for Networks of Tick Tock Automata (NTTA)") + ("show this message") + | lyra::opt(verbosity, "0-6") + ["-v"]["--verbosity"]("set verbosity level, default: " + std::to_string(verbosity)) + | lyra::opt(show_version) + ["-V"]["--version"]("show version") + | lyra::opt(input, "DIR") + ["-f"]["--input"]("add input directory to parse and verify").required() + | lyra::opt(plugin_dirs, "DIR") + ["-d"]["--plugin-dir"]("use a directory to look for plugins") + | lyra::opt(parser, "PARSER") + ["-p"]["--parser"]("set a parser to use, default: " + parser) + | lyra::opt(list_plugins) + ["-L"]["--list-plugins"]("list found plugins and exit") + | lyra::opt(ignore, "GLOB") + ["-i"]["--ignore"]("add a glob file pattern to ignore") + | lyra::opt(query, "CTL") + ["-Q"]["--query"]("add a CTL query to check verify") + | lyra::opt(query_files, "FILE") + ["-q"]["--query-file"]("add a json file with CTL queries to check verify") + | lyra::opt(pick_strategy, "STRATEGY").choices("first", "last", "random") + ["-s"]["--pick-strategy"]("waiting list pick strategy, default: " + pick_strategy) + | lyra::opt(disabled_warnings, "WARN") + ["-w"]["--disable-warning"]("disable a warning") + | lyra::opt(list_warnings) + ["-W"]["--list-warnings"]("list all available warnings and exit") + | lyra::opt(no_warnings) + ["-m"]["--no-warnings"]("disable all warnings") + | lyra::opt(result_file, "FILE") + ["-t"]["--result-file"]("set file to output results to") + | lyra::opt(output_json) + ["-j"]["--result-json"]("output results in json format") + ; + auto args = cli.parse({argc, argv}); + if(show_help) { + std::cout << cli << std::endl; + return 0; + } + if(verbosity < 0 || verbosity > SPDLOG_LEVEL_OFF) { + std::cout << "verbosity must be within 0-6" << std::endl; + return 1; + } + spdlog::set_level(static_cast(SPDLOG_LEVEL_OFF - verbosity)); + spdlog::trace("welcome to {} v{}", PROJECT_NAME, PROJECT_VER); + if(show_version) { + std::cout << PROJECT_NAME << " v" << PROJECT_VER << std::endl; + return 0; + } + if(!args) { + spdlog::error(args.message()); + return 1; + } + if(list_warnings) { + std::cout << "[WARNINGS]:\n"; + for(const auto& warning : aaltitoad::warnings::descriptions()) + std::cout << "\t - [" << magic_enum::enum_name(warning.first) << "]: " << warning.second << "\n"; + return 0; + } + if(no_warnings) aaltitoad::warnings::disable_all(); - disable_warnings(cli_arguments["disable-warn"].as_list_or_default({})); + disable_warnings(disabled_warnings); - auto available_plugins = load_plugins(cli_arguments); - if(cli_arguments["list-plugins"]) { + auto available_plugins = aaltitoad::plugins::load(plugin_dirs); + if(list_plugins) { std::cout << "available plugins:\n" << available_plugins; return 0; } - auto selected_parser = cli_arguments["parser"].as_string_or_default("huppaal_parser"); - if(!available_plugins.contains(selected_parser) || available_plugins.at(selected_parser).type != plugin_type::parser) { - spdlog::critical("no such parser available: '{0}'", selected_parser); + if(!available_plugins.contains(parser) || available_plugins.at(parser).type != plugin_type::parser) { + spdlog::critical("no such parser available: '{}'", parser); return 1; } - spdlog::debug("parsing with {0} plugin", selected_parser); - auto inputs = cli_arguments["input"].as_list(); - auto ignore = cli_arguments["ignore"].as_list_or_default({}); - auto parser = std::get(available_plugins.at(selected_parser).function)(); + spdlog::debug("parsing with {0} plugin", parser); + auto p = std::get(available_plugins.at(parser).function)(); ya::timer t{}; - auto parse_result = parser->parse_files(inputs, ignore); + auto parse_result = p->parse_files(input, ignore); for(auto& diagnostic : parse_result.diagnostics) aaltitoad::warnings::print_diagnostic(diagnostic); if(!parse_result.result.has_value()) { spdlog::error("compilation failed"); return 1; } + auto n = std::move(parse_result.result.value()); trace_log_ntta(*n); spdlog::debug("model parsing took {0}ms", t.milliseconds_elapsed()); @@ -87,22 +147,21 @@ int main(int argc, char** argv) { t.start(); std::vector queries{}; aaltitoad::ctl_interpreter ctl_compiler{n->symbols, n->external_symbols}; - for(auto& q : cli_arguments["query"].as_list_or_default({})) { + for(auto& q : query) { spdlog::trace("compiling query '{0}'", q); auto qq = ctl_compiler.compile(q); std::stringstream ss{}; ss << qq; spdlog::trace("resulting tree: {0}", ss.str()); queries.emplace_back(qq); } - for(auto& f : cli_arguments["query-file"].as_list_or_default({})) { + for(auto& f : query_files) { spdlog::trace("loading queries in file {0}", f); auto json_queries = aaltitoad::load_query_json_file(f, {n->symbols, n->external_symbols}); queries.insert(queries.end(), json_queries.begin(), json_queries.end()); } spdlog::debug("query parsing took {0}ms", t.milliseconds_elapsed()); - auto strategy_s = cli_arguments["pick-strategy"].as_string_or_default("first"); - auto strategy = magic_enum::enum_cast(strategy_s).value_or(aaltitoad::pick_strategy::first); + auto strategy = magic_enum::enum_cast(pick_strategy).value_or(aaltitoad::pick_strategy::first); spdlog::debug("using pick strategy '{0}'", magic_enum::enum_name(strategy)); n->add_tocker(std::make_unique()); @@ -115,12 +174,11 @@ int main(int argc, char** argv) { // open the results file (std::cout by default) spdlog::trace("opening results file stream"); auto* trace_stream = &std::cout; - auto trace_file = cli_arguments["trace-file"].as_string_or_default(""); - if(trace_file != "") - trace_stream = new std::ofstream{trace_file, std::ios::app}; + if(result_file.has_value()) + trace_stream = new std::ofstream{result_file.value(), std::ios::app}; // write json to results file or non-json if not provided - if(cli_arguments["result-json"]) { + if(output_json) { spdlog::trace("gathering results json data"); auto json_results = "[]"_json; for(auto& result : results) { @@ -150,16 +208,6 @@ int main(int argc, char** argv) { } } -auto load_plugins(std::map& cli_arguments) -> plugin_map_t { - auto rpath = std::getenv("AALTITOAD_LIBPATH"); - std::vector look_dirs = { ".", "lib", "plugins" }; - if(rpath) - look_dirs.emplace_back(rpath); - auto provided_dirs = cli_arguments["plugin-dir"].as_list_or_default({}); - look_dirs.insert(look_dirs.end(), provided_dirs.begin(), provided_dirs.end()); - return aaltitoad::plugins::load(look_dirs); -} - void trace_log_ntta(const aaltitoad::ntta_t& n) { if(spdlog::get_level() >= spdlog::level::trace) { std::stringstream internal_symbols_ss{}; @@ -195,3 +243,13 @@ void trace_log_ntta(const aaltitoad::ntta_t& n) { } } +void disable_warnings(const std::vector& disable_warns) { + aaltitoad::warnings::enable_all(); + for(auto& w : disable_warns) { + auto opt = magic_enum::enum_cast(w); + if(opt.has_value()) + aaltitoad::warnings::disable_warning(opt.value()); + else + spdlog::warn("not a warning: {0}", w); + } +} diff --git a/src/plugin_system/plugin_system.cpp b/src/plugin_system/plugin_system.cpp index d359c55..5d859c6 100644 --- a/src/plugin_system/plugin_system.cpp +++ b/src/plugin_system/plugin_system.cpp @@ -32,15 +32,20 @@ namespace aaltitoad::plugins { return val; } - plugin_map_t load(const std::vector &search_directories) { + plugin_map_t load(const std::vector& plugin_dirs) { + auto rpath = std::getenv("AALTITOAD_LIBPATH"); + std::vector look_dirs = { ".", "lib", "plugins" }; + if(rpath) + look_dirs.emplace_back(rpath); + look_dirs.insert(look_dirs.end(), plugin_dirs.begin(), plugin_dirs.end()); plugin_map_t loaded_plugins{}; - for (auto &directory: search_directories) { - if (!std::filesystem::exists(directory)) { + for(auto& directory : look_dirs) { + if(!std::filesystem::exists(directory)) { spdlog::trace("does not exist: {0}", directory); continue; } spdlog::trace("searching for plugins in: {0}", directory); - for (const auto &entry: std::filesystem::directory_iterator(directory)) { + for(const auto& entry : std::filesystem::directory_iterator(directory)) { try { if (!entry.is_regular_file()) continue; @@ -52,9 +57,9 @@ namespace aaltitoad::plugins { auto stem = std::string(load_symbol(handle, "get_plugin_name")()); auto type = static_cast(load_symbol(handle, "get_plugin_type")()); auto version = std::string(load_symbol(handle, "get_plugin_version")()); - if (loaded_plugins.contains(stem)) + if(loaded_plugins.contains(stem)) throw std::logic_error("plugin with name '" + stem + "' is already loaded. All plugins must have unique names"); - switch (type) { + switch(type) { case plugin_type::tocker: { auto ctor = load_symbol(handle, "create_tocker"); loaded_plugins.insert(std::make_pair(stem, plugin_t{type, version, ctor})); diff --git a/src/plugin_system/plugin_system.h b/src/plugin_system/plugin_system.h index 31cae5c..99d22d7 100644 --- a/src/plugin_system/plugin_system.h +++ b/src/plugin_system/plugin_system.h @@ -68,7 +68,7 @@ using plugin_map_t = std::map; std::ostream& operator<<(std::ostream&, const plugin_map_t&); namespace aaltitoad::plugins { - plugin_map_t load(const std::vector &search_directories); + plugin_map_t load(const std::vector& plugin_dirs); } #endif //AALTITOAD_PLUGIN_SYSTEM_H