feat: trace as json

Author: Asger Gitz-Johansen

src/cli/verifier/cli_options.h

@@ -45,7 +45,8 @@ std::vector<option_t> get_options() {
             {"list-warn",     'W', argument_requirement::NO_ARG,       "List all warnings available"},
             {"no-warn",       'm', argument_requirement::NO_ARG,       "Disable all warnings"},
 
-            {"trace-file",    't', argument_requirement::REQUIRE_ARG,  "Provide file to output result-traces to. Default is stdout"}, // TODO: We should output JSON formatted traces
+            {"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>
@@ -104,21 +105,39 @@ int main(int argc, char** argv) {
         auto results = frs.is_reachable(*n, queries);
         spdlog::info("reachability search took {0}ms", t.milliseconds_elapsed());
 
-        // gather and return results
-        auto trace_file = cli_arguments["trace-file"].as_string_or_default("");
+        // 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};
-        for(auto& result : results) {
-            *trace_stream << result.query << ": " << std::boolalpha << result.solution.has_value() << "\n";
-            if(result.solution.has_value())
-                *trace_stream << result.solution.value(); // TODO: This should be json formatted
+
+        // 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;
     } catch (std::exception& any) {
         spdlog::error(any.what());
-        std::cout.flush(); // Flush the output streams, just to be nice
+        std::cout.flush();
         std::cerr.flush();
         return 1;
     }

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

@@ -112,3 +112,16 @@ auto operator<<(std::ostream& o, const aaltitoad::forward_reachability_searcher:
         o << s->second.parent.value();
     return o << s->second.data;
 }
+
+void to_json_helper(const aaltitoad::forward_reachability_searcher::solution_t& s, std::vector<nlohmann::json>& tail) {
+    if(s->second.parent.has_value())
+        to_json_helper(s->second.parent.value(), tail);
+    tail.push_back(s->second.data.to_json());
+}
+
+auto to_json(const aaltitoad::forward_reachability_searcher::solution_t& s) -> std::vector<nlohmann::json> {
+    std::vector<nlohmann::json> states{};
+    to_json_helper(s, states);
+    return states;
+}
+

src/verification/forward_reachability.cpp

@@ -21,6 +21,7 @@
 #include "ntta/tta.h"
 #include "traceable_multimap.h"
 #include <ctl_syntax_tree.h>
+#include <nlohmann/json.hpp>
 #include <vector>
 #include <utility>
 
@@ -51,5 +52,6 @@ namespace aaltitoad {
     };
 }
 auto operator<<(std::ostream& o, const aaltitoad::forward_reachability_searcher::solution_t& s) -> std::ostream&;
+auto to_json(const aaltitoad::forward_reachability_searcher::solution_t& s) -> std::vector<nlohmann::json>;
 
 #endif //AALTITOAD_FORWARD_REACHABILITY_H