feat: Add ntta builder that works on strings

CMakeLists.txt

@@ -30,6 +30,7 @@ set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
 set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR})
 
 add_compile_definitions(DEFAULT_EXPRESSION_VALUE="true")
+# TODO: Implement timers/clocks-support
 CPMAddPackage(NAME expr GIT_TAG fix/multiple-use-compatibility GITHUB_REPOSITORY sillydan1/expr OPTIONS "ENABLE_Z3 ON")
 CPMAddPackage(NAME argvparse VERSION 1.2.3 GITHUB_REPOSITORY sillydan1/argvparse)
 CPMAddPackage(NAME ctl-expr GIT_TAG main GITHUB_REPOSITORY sillydan1/ctl-expr)
@@ -80,7 +81,8 @@ include_directories(
         src
 )
 set(${PROJECT_NAME}_SOURCES
-        src/ntta/ntta_builder.cpp
+        src/ntta/builder/ntta_builder.cpp
+        src/ntta/builder/ntta_builder_2.cpp
         src/ntta/tta.cpp
         src/ntta/interesting_tocker.cpp
         src/plugin_system/plugin_system.cpp

src/ntta/ntta_builder.h → src/ntta/builder/ntta_builder.h

@@ -1,7 +1,7 @@
 #ifndef AALTITOAD_NTTA_BUILDER_H
 #define AALTITOAD_NTTA_BUILDER_H
-#include "tta.h"
-#include "interesting_tocker.h"
+#include "ntta/tta.h"
+#include "ntta/interesting_tocker.h"
 
 namespace aaltitoad {
     struct tta_builder {
@@ -38,6 +38,7 @@ namespace aaltitoad {
         auto add_symbols(const expr::symbol_table_t& ss) -> ntta_builder&;
         auto add_external_symbol(const symbol_value_pair& symbol) -> ntta_builder&;
         auto add_external_symbols(const std::vector<symbol_value_pair>& ss) -> ntta_builder&;
+        auto add_external_symbols(const expr::symbol_table_t& ss) -> ntta_builder&;
         auto build() const -> ntta_t;
         auto build_heap() const -> ntta_t*;
         auto build_with_interesting_tocker() const -> ntta_t;

src/ntta/builder/ntta_builder_2.cpp

@@ -0,0 +1,102 @@
+#include "ntta_builder_2.h"
+#include "ntta_builder.h"
+
+namespace aaltitoad {
+
+    auto tta_builder2::set_instance_name(const std::string& name) -> tta_builder2& {
+        instance_name = name;
+        return *this;
+    }
+
+    auto tta_builder2::set_symbol_declarations(const std::string& decls) -> tta_builder2& {
+        symbol_declarations = decls;
+        return *this;
+    }
+
+    auto tta_builder2::add_sub_tta(const std::string& tta_name, const std::string& arguments) -> tta_builder2& {
+        sub_tta_instances.push_back({tta_name, arguments});
+        return *this;
+    }
+
+    auto tta_builder2::add_location(const std::string &name) -> tta_builder2 & {
+        locations.insert(name);
+        return *this;
+    }
+
+    auto tta_builder2::set_start_location(const std::string &name) -> tta_builder2 & {
+        initial_location = name;
+        return *this;
+    }
+
+    auto tta_builder2::set_main() -> tta_builder2 & {
+        is_main = true;
+        return *this;
+    }
+
+    auto tta_builder2::add_edge(const edge_builder2 &edge) -> tta_builder2 & {
+        edges.push_back(edge);
+        return *this;
+    }
+
+    auto tta_builder2::build(expr::symbol_table_t& symbols, expr::symbol_table_t& external_symbols) -> tta_builder {
+        tta_builder b{symbols, external_symbols};
+        for(auto& loc : locations)
+            b.add_location(loc);
+        b.set_starting_location(initial_location);
+        for(auto& edge : edges)
+            b.add_edge({edge.source, edge.target, edge.guard, edge.update});
+        return b;
+    }
+
+    auto ntta_builder2::add_declarations(const std::string& decls) -> ntta_builder2& {
+        symbol_declarations.push_back(decls);
+        return *this;
+    }
+
+    auto ntta_builder2::add_external_declarations(const std::string& decls) -> ntta_builder2& {
+        external_symbol_declarations.push_back(decls);
+        return *this;
+    }
+
+    auto ntta_builder2::add_tta(const tta_builder2& builder) -> ntta_builder2& {
+        tta_builders.insert({builder.instance_name, builder});
+        return *this;
+    }
+
+    auto ntta_builder2::build() -> ntta_builder {
+        expr::symbol_table_t s{}, e{};
+        expr::interpreter i{s};
+        for(auto& tta : tta_builders)
+            s += i.interpret_declarations(tta.second.symbol_declarations);
+        for(auto& d : symbol_declarations)
+            s += i.interpret_declarations(d);
+        for(auto& d : external_symbol_declarations)
+            e += i.interpret_declarations(d);
+        // TODO: Implement support for declarations that are initialized with other variables.
+        //       One way of doing this could be:
+        //       - remember which decl-strings fail
+        //       - try once more to load previously failed decl-strings (throw if fails on this second try)
+        //       Or we could do some dependency-graph detection (read up on static analysis tools)
+        ntta_builder b{};
+        b.add_symbols(s).add_external_symbols(e);
+        // TODO: Check for dependency loops with tarjans SCC algorithm
+        auto main_component = std::find_if(tta_builders.begin(), tta_builders.end(),
+                                           [](const auto& t){ return t.second.is_main; });
+        if(main_component == tta_builders.end())
+            throw std::logic_error("no main tta");
+        build_recursive(b, main_component->first, main_component, s, e);
+        return b;
+    }
+
+    // TODO: Sequential composition
+    void ntta_builder2::build_recursive(ntta_builder &builder, const std::string& name, const tta_builder2_it &it, expr::symbol_table_t& s, expr::symbol_table_t& e) {
+        auto bb = it->second.build(s,e);
+        builder.add_tta(name, bb);
+        for(auto& subtta : it->second.sub_tta_instances) {
+            auto itt = tta_builders.find(subtta.filename);
+            if(itt == tta_builders.end())
+                spdlog::error("no such tta: {}", subtta.filename);
+            build_recursive(builder, subtta.parameterization, itt, s, e);
+        }
+    }
+}

src/ntta/builder/ntta_builder_2.h

@@ -0,0 +1,54 @@
+#ifndef AALTITOAD_NTTA_BUILDER_2_H
+#define AALTITOAD_NTTA_BUILDER_2_H
+#include <map>
+#include <vector>
+#include <string>
+#include <set>
+#include <ntta/tta.h>
+#include "ntta_builder.h"
+
+// TODO: This two-layer builder structure should be refactored...
+namespace aaltitoad {
+    // TODO: Rename to something else
+    struct edge_builder2 {
+        std::string source, target, guard{}, update{};
+    };
+
+    struct sub_tta {
+        std::string filename, parameterization;
+    };
+
+    // TODO: Rename to something else
+    struct tta_builder2 {
+        auto set_instance_name(const std::string& name) -> tta_builder2&;
+        auto set_symbol_declarations(const std::string& decls) -> tta_builder2&;
+        auto add_sub_tta(const std::string& tta_name, const std::string& arguments) -> tta_builder2&;
+        auto add_location(const std::string& name) -> tta_builder2&;
+        auto set_start_location(const std::string& name) -> tta_builder2&;
+        auto set_main() -> tta_builder2&;
+        auto add_edge(const edge_builder2& edge) -> tta_builder2&;
+        auto build(expr::symbol_table_t& symbols, expr::symbol_table_t& external_symbols) -> tta_builder;
+        std::string instance_name{};
+        std::string symbol_declarations{};
+        std::string initial_location{};
+        bool is_main = false;
+        std::set<std::string> locations{};
+        std::vector<edge_builder2> edges{};
+        std::vector<sub_tta> sub_tta_instances{};
+    };
+
+    // TODO: Rename to something else
+    struct ntta_builder2 {
+        using tta_builder2_it = std::map<std::string, tta_builder2>::iterator;
+        auto add_declarations(const std::string& decls) -> ntta_builder2&;
+        auto add_external_declarations(const std::string& decls) -> ntta_builder2&;
+        auto add_tta(const tta_builder2& builder) -> ntta_builder2&;
+        auto build() -> ntta_builder;
+        void build_recursive(ntta_builder& builder, const std::string& name, const tta_builder2_it& it, expr::symbol_table_t& s, expr::symbol_table_t& e);
+        std::map<std::string, tta_builder2> tta_builders;
+        std::vector<std::string> symbol_declarations;
+        std::vector<std::string> external_symbol_declarations;
+    };
+}
+
+#endif //AALTITOAD_NTTA_BUILDER_2_H

src/parser/CMakeLists.txt

@@ -1,3 +1,7 @@
 project(parser_plugins VERSION 1.0.0)
 add_library(huppaal_parser SHARED huppaal_parser.cpp)
 target_link_libraries(huppaal_parser PUBLIC aaltitoad expr)
+if(${CODE_COVERAGE})
+    target_link_options(huppaal_parser PUBLIC --coverage)
+    target_compile_options(huppaal_parser PUBLIC --coverage)
+endif()

src/parser/huppaal_parser.cpp

@@ -3,10 +3,11 @@
 #include <fstream>
 #include <nlohmann/json.hpp>
 #include <spdlog/spdlog.h>
+#include <ntta/builder/ntta_builder_2.h>
 
 namespace aaltitoad::huppaal {
     auto load(const std::vector<std::string>& filepaths, const std::vector<std::string> &ignore_list) -> aaltitoad::ntta_t* {
-        aaltitoad::ntta_builder builder{};
+        aaltitoad::ntta_builder2 builder{};
         for(const auto& filepath : filepaths) {
             for(const auto &entry: std::filesystem::directory_iterator(filepath)) {
                 try {
@@ -15,49 +16,45 @@ namespace aaltitoad::huppaal {
 
                     std::ifstream input_filestream(entry.path());
                     auto json_file = nlohmann::json::parse(input_filestream);
-                    builder.add_symbols(load_declarations(json_file, builder.symbols));
+                    load_declarations(builder, json_file);
                     if(json_file.contains("name"))
-                        builder.add_tta(json_file["name"], load_tta(json_file, builder.symbols).build());
+                        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());
                     throw e;
                 }
             }
         }
-        return builder.build_heap();
+        return builder.build().build_heap();
     }
 
-    auto load_declarations(const nlohmann::json& json_file, const expr::symbol_table_t& symbols) -> expr::symbol_table_t {
-        expr::symbol_table_t result{};
-        expr::interpreter i{symbols};
+    void load_declarations(ntta_builder2& b, const nlohmann::json& json_file) {
         if(json_file.contains("declarations"))
-            result += i.interpret_declarations(json_file["declarations"]);
+            b.add_declarations(json_file["declarations"]);
         if(json_file.contains("parts"))
             for(auto& p : json_file["parts"])
-                result += load_part(p);
-        return result;
+                // TODO: Missing external/internal check
+                b.add_external_declarations(load_part(p));
     }
 
-    // TODO: Missing external/internal check
-    auto load_part(const nlohmann::json& json_file) -> expr::symbol_table_t {
-        expr::symbol_table_t result{{}};
-        expr::symbol_value_t val{};
-        val <<= json_file["SpecificType"]["Variable"]["Value"];
-        result[json_file["PartName"]] = val;
-        return result;
+    auto load_part(const nlohmann::json& json_file) -> std::string {
+        std::stringstream ss{};
+        ss << json_file["PartName"] << " := " << json_file["SpecificType"]["Variable"]["Value"];
+        return ss.str();
     }
 
-    auto load_tta(const nlohmann::json& json_file, expr::symbol_table_t& symbols) -> aaltitoad::tta_builder {
-        expr::symbol_table_t externals{}; // TODO: actual externals
-        aaltitoad::tta_builder builder{symbols, externals};
-        builder.set_starting_location(json_file["initial_location"]["id"]);
+    auto load_tta(const nlohmann::json& json_file) -> aaltitoad::tta_builder2 {
+        aaltitoad::tta_builder2 builder{};
+        builder.set_start_location(json_file["initial_location"]["id"]);
         for(auto& loc : json_file["locations"])
             builder.add_location(loc["id"]);
-        // TODO: stitch "final_location" together with "initial_location"
-        // TODO: recurse on sub_components (sequential/parallel composition)
-        for(auto& edge : json_file["edges"])
-            builder.add_edge({edge["source_location"], edge["target_location"],
-                              (std::string)edge["guard"], (std::string)edge["update"]});
+        for(auto& edge : json_file["edges"]) {
+            auto target_loc = edge["target_location"];
+            if(edge["target_location"] == json_file["final_location"]["id"])
+                target_loc = builder.initial_location;
+            builder.add_edge({edge["source_location"], target_loc,
+                              (std::string) edge["guard"], (std::string) edge["update"]});
+        }
         return builder;
     }
 }

src/parser/huppaal_parser.h

@@ -1,14 +1,15 @@
 #ifndef AALTITOAD_HUPPAAL_PARSER_H
 #define AALTITOAD_HUPPAAL_PARSER_H
 #include "plugin_system/plugin_system.h"
-#include "ntta/ntta_builder.h"
+#include "ntta/builder/ntta_builder.h"
+#include "ntta/builder/ntta_builder_2.h"
 #include <nlohmann/json.hpp>
 
 namespace aaltitoad::huppaal {
-    auto load_declarations(const nlohmann::json& json_file, const expr::symbol_table_t& symbols) -> expr::symbol_table_t;
-    auto load_part(const nlohmann::json& json_file) -> expr::symbol_table_t;
+    void load_declarations(ntta_builder2& b, const nlohmann::json& json_file);
+    auto load_part(const nlohmann::json& json_file) -> std::string;
     auto load(const std::vector<std::string>& filepaths, const std::vector<std::string> &ignore_list) -> aaltitoad::ntta_t*;
-    auto load_tta(const nlohmann::json& json_file, expr::symbol_table_t& symbols) -> aaltitoad::tta_builder;
+    auto load_tta(const nlohmann::json& json_file) -> aaltitoad::tta_builder2;
 }
 
 #endif //AALTITOAD_HUPPAAL_PARSER_H

test/verification/forward_reachability_tests.cpp

@@ -1,6 +1,6 @@
 #include <ntta/tta.h>
 #include <catch2/catch_test_macros.hpp>
-#include <ntta/ntta_builder.h>
+#include <ntta/builder/ntta_builder.h>
 #include <verification/forward_reachability.h>
 
 SCENARIO("basic reachability", "[frs]") {