Merge pull request #47 from sillydan1/dev

Improvements found during testing

Author: sillydan1

.gitignore

@@ -43,5 +43,6 @@ test/**/results.txt
 # neovim autogenerated files
 compile_commands.json
 Debug/
+Release/
 .cache/
 

.vscode/launch.json

@@ -19,7 +19,9 @@
             "args": [ 
                 "-f", "../test/verification/fischer-suite/fischer-2/",
                 "-q", "../test/verification/fischer-suite/fischer-2/Queries.json",
-                "-i", ".*\\.ignore.*"
+                "-i", ".*\\.ignore.*",
+                "-t", "/dev/null",
+                "-v", "6"
             ]
         }
     ]

CMakeLists.txt

@@ -14,7 +14,7 @@
 #   You should have received a copy of the GNU General Public License
 #   along with this program.  If not, see <https://www.gnu.org/licenses/>.
 cmake_minimum_required(VERSION 3.16) # 3.16+ because of target_precompiled_header
-project(aaltitoad VERSION 1.1.0)
+project(aaltitoad VERSION 1.2.0)
 set(THREADS_PREFER_PTHREAD_FLAG ON)
 set(CMAKE_CXX_STANDARD 20)
 set(CXX_STANDARD_REQUIRED ON)

src/cli/verifier/cli_options.h

@@ -17,6 +17,7 @@
  */
 #ifndef AALTITOAD_CLI_OPTIONS_H
 #define AALTITOAD_CLI_OPTIONS_H
+#include "arguments.h"
 #include <vector>
 #include <argvparse.h>
 #include <iostream>
@@ -26,21 +27,26 @@
 
 std::vector<option_t> 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"},
+            {"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"},
+            {"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"},
+            {"pick-strategy", 's', argument_requirement::REQUIRE_ARG,  "Waiting list pick strategy [first|last|random]. Default is first"},
 
-            {"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"},
+            {"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"},
     };
 }
 

src/cli/verifier/main.cpp

@@ -17,6 +17,7 @@
  */
 #include <aaltitoadpch.h>
 #include <ctl_syntax_tree.h>
+#include <ios>
 #include <ntta/tta.h>
 #include <timer>
 #include <plugin_system/plugin_system.h>
@@ -27,9 +28,11 @@
 #include <expr-lang/expr-scanner.hpp>
 #include <expr-lang/expr-parser.hpp>
 #include "expr-wrappers/ctl-interpreter.h"
+#include "magic_enum.hpp"
 #include "query/query_json_loader.h"
 #include "spdlog/common.h"
 #include "spdlog/spdlog.h"
+#include "verification/pick_strategy.h"
 
 auto load_plugins(std::map<std::string, argument_t>& cli_arguments) -> plugin_map_t;
 void trace_log_ntta(const aaltitoad::ntta_t& n);
@@ -91,18 +94,44 @@ int main(int argc, char** argv) {
         }
         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<aaltitoad::pick_strategy>(strategy_s).value_or(aaltitoad::pick_strategy::first);
+        spdlog::debug("using pick strategy '{0}'", magic_enum::enum_name(strategy));
+
         n->add_tocker(std::make_unique<aaltitoad::interesting_tocker>());
         spdlog::trace("starting reachability search for {0} queries", queries.size());
         t.start();
-        aaltitoad::forward_reachability_searcher frs{};
+        aaltitoad::forward_reachability_searcher frs{strategy};
         auto results = frs.is_reachable(*n, queries);
-        spdlog::debug("reachability search took {0}ms", t.milliseconds_elapsed());
-
-        // gather and return results
-        for(auto& result : results) {
-            std::cout << result.query << ": " << std::boolalpha << result.solution.has_value() << "\n";
-            if(result.solution.has_value())
-                std::cout << result.solution.value();
+        spdlog::info("reachability search took {0}ms", t.milliseconds_elapsed());
+
+        // 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};
+
+        // write json to results file or non-json if not provided
+        if(cli_arguments["result-json"]) {
+            spdlog::trace("gathering results json data");
+            auto json_results = "[]"_json;
+            for(auto& result : results) {
+                nlohmann::json res{};
+                std::stringstream ss{}; ss << result.query;
+                res["query"] = ss.str();
+                if(result.solution.has_value())
+                    res["trace"] = to_json(result.solution.value());
+                json_results.push_back(res);
+            }
+            *trace_stream << json_results << std::endl;
+        } else {
+            spdlog::trace("printing resuls data (non-json)");
+            for(auto& result : results) {
+                *trace_stream << result.query << ": " << std::boolalpha << result.solution.has_value();
+                if(result.solution.has_value())
+                    *trace_stream << result.solution.value();
+            }
         }
 
         return 0;

src/cli/verifier/query/query_json_loader.cpp

@@ -73,8 +73,10 @@ namespace aaltitoad {
                         if(v.operator_type == ctl::modal_op_t::E && std::get<ctl::quantifier_t>(c.node).operator_type == ctl::quantifier_op_t::F)
                             return is_query_trivial(cc);
 
-                        if(v.operator_type == ctl::modal_op_t::A && std::get<ctl::quantifier_t>(c.node).operator_type == ctl::quantifier_op_t::G)
-                            return is_query_trivial(cc);
+                        if(v.operator_type == ctl::modal_op_t::A && std::get<ctl::quantifier_t>(c.node).operator_type == ctl::quantifier_op_t::G) {
+                            spdlog::debug("safety queries (A G <query>) are not supported yet. See issue #41 if you need this feature");
+                            return false;
+                        }
 
                         return false;
                     },

src/ntta/ntta_state_json.h

@@ -183,6 +183,28 @@ namespace aaltitoad {
         ss << *this;
         return ss.str();
     }
+
+    auto ntta_t::to_json() const -> nlohmann::json {
+        nlohmann::json result{};
+        result["locations"] = "[]"_json;
+        for(auto& component : components) {
+            auto j = "{}"_json;
+            j[component.first] = component.second.current_location->first;
+            result["locations"].push_back(j);
+        }
+        result["symbols"] = "{}"_json;
+        for(auto& symbol : symbols + external_symbols) {
+            std::visit(ya::overload(
+                        [&result, &symbol](const int& v){ result["symbols"][symbol.first] = v; },
+                        [&result, &symbol](const float& v){ result["symbols"][symbol.first] = v; },
+                        [&result, &symbol](const bool& v){ result["symbols"][symbol.first] = v; },
+                        [&result, &symbol](const std::string& v){ result["symbols"][symbol.first] = v; },
+                        [&result, &symbol](const expr::clock_t& v){ result["symbols"][symbol.first] = v.time_units; },
+                        [&result, &symbol](auto&& v){ result["symbols"][symbol.first] = "undefined"; }
+                        ), static_cast<const expr::underlying_symbol_value_t&>(symbol.second));
+        }
+        return result;
+    }
 }
 
 auto operator<<(std::ostream& os, const aaltitoad::ntta_t& state) -> std::ostream& {

src/ntta/tta.cpp

@@ -18,6 +18,7 @@
 #ifndef AALTITOAD_TTA_H
 #define AALTITOAD_TTA_H
 #include "expr-wrappers/interpreter.h"
+#include <nlohmann/json.hpp>
 #include <string>
 #include <graph>
 #include <symbol_table.h>
@@ -117,6 +118,7 @@ namespace aaltitoad {
         void apply(const std::vector<expr::symbol_table_t>& external_symbol_change_list);
         void apply_internal(const expr::symbol_table_t& symbol_changes);
         auto to_string() const -> std::string;
+        auto to_json() const -> nlohmann::json;
     private:
         class tick_resolver {
         public:

src/ntta/tta.h

@@ -20,6 +20,7 @@
 #include "scoped_interpreter.h"
 #include "spdlog/spdlog.h"
 #include "util/string_extensions.h"
+#include "util/warnings.h"
 #include <ntta/builder/ntta_builder.h>
 #include <util/exceptions/parse_error.h>
 
@@ -89,7 +90,7 @@ namespace aaltitoad::hawk {
             auto interpreter = construct_interpreter_from_scope(instance, scoped_name);
             auto decls = interpreter.parse_declarations(instance_template.declarations);
             if(internal_symbols.is_overlapping(decls))
-                spdlog::warn("double declaration detected");
+                warnings::warn(parser_warning, "double declaration detected");
             internal_symbols += decls;
 
             call_func_aggregate_errors(instance_template.instances, [this, &scoped_name](auto& template_instance){