feat: add query file and direct query to verifier cli

src/cli/verifier/CMakeLists.txt

@@ -1,6 +1,6 @@
 project(verifier VERSION 1.0.0)
 find_package(argvparse REQUIRED)
-add_executable(${PROJECT_NAME} main.cpp)
+add_executable(${PROJECT_NAME} main.cpp query_json_loader.cpp)
 target_link_libraries(${PROJECT_NAME} aaltitoad ctl argvparse)
 if(TARGET default_plugins)
     add_dependencies(${PROJECT_NAME} default_plugins)

src/cli/verifier/cli_options.h

@@ -15,6 +15,8 @@ std::vector<option_t> get_options() {
             {"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"},
 
             {"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"},
@@ -33,6 +35,10 @@ bool is_required(const std::string& s) {
 bool is_required_provided(std::map<std::string, argument_t>& provided_args, const std::vector<option_t>& 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;

src/cli/verifier/main.cpp

@@ -6,6 +6,7 @@
 #include <verification/forward_reachability.h>
 #include "cli_options.h"
 #include "../cli_common.h"
+#include "query_json_loader.h"
 
 auto load_plugins(std::map<std::string, argument_t>& cli_arguments) -> plugin_map_t;
 
@@ -45,17 +46,25 @@ int main(int argc, char** argv) {
     std::unique_ptr<aaltitoad::ntta_t> n{parser(inputs, ignore)};
     spdlog::debug("model parsing took {0}ms", t.milliseconds_elapsed());
 
-    // TODO: load the queries
     t.start();
-    auto s = n->symbols + n->external_symbols;
-    auto query = ctl::compiler{{s}}.compile("E F pubid == 1");
+    std::vector<ctl::compiler::compiled_expr_t> queries{};
+    ctl::compiler ctl_compiler{{n->symbols, n->external_symbols}};
+    for(auto& q : cli_arguments["query"].as_list_or_default({})) {
+        spdlog::trace("compiling query '{0}'", q);
+        queries.emplace_back(ctl_compiler.compile(q));
+    }
+    for(auto& f : cli_arguments["query-file"].as_list_or_default({})) {
+        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());
 
     // TODO: filter unsupported queries out
 
     t.start();
     aaltitoad::forward_reachability_searcher frs{};
-    auto results = frs.is_reachable(*n, query);
+    auto results = frs.is_reachable(*n, queries);
     spdlog::debug("reachability search took {0}ms", t.milliseconds_elapsed());
     for(auto& result : results) {
         std::cout << result.query << ": " << std::boolalpha << result.solution.has_value() << "\n";

src/cli/verifier/query_json_loader.cpp

@@ -0,0 +1,22 @@
+#include <drivers/driver.h>
+#include <nlohmann/json.hpp>
+#include "query_json_loader.h"
+
+namespace aaltitoad {
+    auto load_query_json_file(const std::string& json_file, std::initializer_list<expr::symbol_table_ref_t> environments) -> std::vector<ctl::compiler::compiled_expr_t> {
+        try {
+            std::vector<ctl::compiler::compiled_expr_t> result{};
+            ctl::compiler c{environments};
+            std::ifstream f(json_file);
+            auto data = nlohmann::json::parse(f);
+            for(auto& q : data) {
+                spdlog::trace("compiling query {0}", q["query"]);
+                result.emplace_back(c.compile(q["query"]));
+            }
+            return result;
+        } catch (std::exception &e) {
+            spdlog::error("unable to parse json file {0}: {1}", json_file, e.what());
+            throw e;
+        }
+    }
+}

src/cli/verifier/query_json_loader.h

@@ -0,0 +1,9 @@
+#ifndef AALTITOAD_QUERY_JSON_LOADER_H
+#define AALTITOAD_QUERY_JSON_LOADER_H
+#include <ctl_compiler.h>
+
+namespace aaltitoad {
+    auto load_query_json_file(const std::string& json_file, std::initializer_list<expr::symbol_table_ref_t> environments) -> std::vector<ctl::compiler::compiled_expr_t>;
+}
+
+#endif //AALTITOAD_QUERY_JSON_LOADER_H

src/parser/huppaal_parser.cpp

@@ -23,7 +23,7 @@ namespace aaltitoad::huppaal {
                     if(json_file.contains("name"))
                         builder.add_tta(load_tta(json_file));
                 } catch (std::exception &e) {
-                    spdlog::error("Unable to parse json file {0}: {1}", entry.path().c_str(), e.what());
+                    spdlog::error("unable to parse json file {0}: {1}", entry.path().c_str(), e.what());
                     throw e;
                 }
             }

src/verification/forward_reachability.cpp

@@ -18,9 +18,10 @@ namespace aaltitoad {
     }
 
     auto forward_reachability_searcher::is_reachable(const aaltitoad::ntta_t& s0, const std::vector<compiled_query_t>& q) -> solutions_t {
-        // TODO: statistics on all return statements (trace)
-        // TODO: Catch SIGTERM (ctrl-c) and write statistics (trace)
+        // TODO: statistics on all return statements (info)
+        // TODO: Catch SIGTERM (ctrl-c) and write statistics (info)
         // TODO: Periodically print waiting list size for debugging purposes (debug)
+        // TODO: Tocking clocks (interestingly) should delay the entire symbol_table
         W = {s0}; P = {}; solutions = empty_solution_set(q);
         auto s0_it = P.add(s0);
         for(auto& l : s0.tock()) {