diff --git a/include/do-verify/ptl.hpp b/include/do-verify/ptl.hpp
index 46249e2..1a2db5a 100644
--- a/include/do-verify/ptl.hpp
+++ b/include/do-verify/ptl.hpp
@@ -35,7 +35,12 @@ struct ptl_parser : ptl_grammar{
   std::unordered_map<NodeKey, int, NodeKeyHash> node_dedup_map;
   std::string last_error;
 
-  int add_or_find_node(const ParsedNode &node) {
+  int add_or_find_node(ParsedNode node) {
+    if (node.type == NodeType::AND || node.type == NodeType::OR) {
+      if (node.leftOperandIndex > node.rightOperandIndex) {
+        std::swap(node.leftOperandIndex, node.rightOperandIndex);
+      }
+    }
     NodeKey key{node.type, node.leftOperandIndex, node.rightOperandIndex, node.a, node.b};
     auto it = node_dedup_map.find(key);
     if (it != node_dedup_map.end()) {
diff --git a/src/MTLEngine.cpp b/src/MTLEngine.cpp
index e4fb02b..6e12dc9 100644
--- a/src/MTLEngine.cpp
+++ b/src/MTLEngine.cpp
@@ -208,6 +208,17 @@ bool run_evaluation(std::vector<DiscreteNode> &nodes, db_interval_set::IntervalS
     
 }
 
+// TODO
+// feature list çıkar (double buffer)
+// testlere bak
+// feature list: binary executable mi / library mi
+// timescales birleştirme
+// random propertyler / doğru olmasına gerek yok
+// bir de timecales gibi doğru olan multi-property
+// text filedan propertyleri okusun binary
+// hyperfine kullan
+// 
+
 bool run_evaluation(std::vector<DiscreteNode> &nodes, std::map<std::string, unsigned int, std::less<>> &proposition_map, db_interval_set::IntervalSetHolder &setHolder, const int time, const std::vector<std::pair<std::string_view, bool>> &propositionInputs) {
     for (const auto &propInput : propositionInputs) {
         auto &propNode = nodes[proposition_map.find(propInput.first)->second];
diff --git a/src/main.cpp b/src/main.cpp
index 159e150..2442844 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -1,14 +1,13 @@
-#include <array>
-#include <cstddef>
 #include <iostream>
 #include <fstream>
 #include <string>
-#include <cstring>
+#include <vector>
 #include <argp.h>
-#include <sys/types.h>
 
-#include <do-verify/binary_row_reader.hpp>
-#include <do-verify/MTLEngine.hpp>
+#include "do-verify/MTLEngine.hpp"
+#include "do-verify/ptl.hpp"
+#include "do-verify/json_feeder.hpp"
+#include "do-verify/interval_set.hpp"
 
 using namespace db_interval_set;
 using namespace do_verify;
@@ -20,43 +19,48 @@ enum RYBINX_OPTS : uint8_t
     OPT_DISCRETE = 'x'
 };
 
-const char *argp_program_version = "do-verify-bin 0.1.0";
+const char *argp_program_version = "do-verify-bin 0.2.0";
 const char *argp_program_bug_address = "Arinc Demir <github.com/arincdemir>";
-static const char *doc = "Do-verify (Reelay) on Binary Row format";
-static const char *args_doc = "SPEC FILE";
+static const char *doc = "Do-verify (Reelay) CLI Tool";
+static const char *args_doc = "TRACE_FILE PROPERTIES_FILE";
 
 struct arguments
 {
-    char *spec;
-    char *file;
+    char *trace_file = nullptr;
+    char *properties_file = nullptr;
     bool dense = false;
     bool discrete = false;
 };
 
-static std::array<struct argp_option, 12> options = {
-    {{"dense", OPT_DENSE, nullptr, 0, "Use dense time model (default)", 0},
-     {"discrete", OPT_DISCRETE, nullptr, 0, "Use discrete time model", 0},
-     {nullptr}}};
+static struct argp_option options[] = {
+    {"dense", OPT_DENSE, nullptr, 0, "Use dense time model (default)", 0},
+    {"discrete", OPT_DISCRETE, nullptr, 0, "Use discrete time model", 0},
+    {nullptr}
+};
 
 static error_t parse_opt(int key, char *arg, struct argp_state *state)
 {
-    auto *arguments = (struct arguments *)state->input;
+    auto *args = (struct arguments *)state->input;
     switch (key)
     {
     case OPT_DENSE:
-        arguments->dense = true;
+        args->dense = true;
         break;
     case OPT_DISCRETE:
-        arguments->discrete = true;
+        args->discrete = true;
         break;
     case ARGP_KEY_ARG:
         if (state->arg_num == 0)
         {
-            arguments->spec = arg;
+            args->trace_file = arg;
+        }
+        else if (state->arg_num == 1)
+        {
+            args->properties_file = arg;
         }
-        else
+        else 
         {
-            arguments->file = arg;
+            return ARGP_ERR_UNKNOWN;
         }
         break;
     case ARGP_KEY_END:
@@ -70,1562 +74,136 @@ static error_t parse_opt(int key, char *arg, struct argp_state *state)
     }
     return 0;
 }
-static struct argp argp = {options.data(), parse_opt, args_doc, doc};
 
-void discrete_case(arguments arguments, std::vector<binary_row_reader::TimescalesInput> allInputs);
-void dense_case(arguments arguments, std::vector<binary_row_reader::TimescalesInput> allInputs);
+static struct argp argp = {options, parse_opt, args_doc, doc};
+
+void discrete_case(const arguments &args);
+void dense_case(const arguments &args);
 
 int main(int argc, char **argv)
 {
-    struct arguments arguments;
-    argp_parse(&argp, argc, argv, 0, nullptr, &arguments);
-
-    // Choices
-    bool use_discrete = arguments.discrete;
-    bool use_dense = arguments.dense;
+    struct arguments args;
+    argp_parse(&argp, argc, argv, 0, nullptr, &args);
 
-    // Apply defaults
-    if (!use_discrete && !use_dense)
+    if (!args.dense && !args.discrete)
     {
-        use_discrete = true;
+        args.dense = true; // Default to dense
     }
 
-    std::ifstream input(arguments.file, std::ios::binary);
-    if (!input)
-    {
-        std::cerr << "Error opening file: " << arguments.file << std::endl;
-        return 1;
-    }
-
-    const auto &allInputs = binary_row_reader::readInputFile(arguments.file);
-
-    if (use_discrete)
+    if (args.discrete)
     {
-        discrete_case(arguments, allInputs);
+        discrete_case(args);
     }
     else
     {
-        dense_case(arguments, allInputs);
+        dense_case(args);
     }
+
+    return 0;
 }
 
-void discrete_case(arguments arguments, std::vector<binary_row_reader::TimescalesInput> allInputs)
+void dense_case(const arguments &args)
 {
-    // AbsentAQ: historically((once[:N]{q}) -> ((not{p}) since {q}))
-    if (strcmp(arguments.spec, "historically((once[:10]{q}) -> ((not{p}) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 10};
-        DiscreteNode notNode{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since{empty(holder), false, NodeType::SINCE, 3, 0, 0, B_INFINITY};
-        DiscreteNode implies{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0};
-        DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, once, notNode, since, implies, always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            //changed these
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:100]{q}) -> ((not{p}) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 100};
-        DiscreteNode notNode{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since{empty(holder), false, NodeType::SINCE, 3, 0, 0, B_INFINITY};
-        DiscreteNode implies{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0};
-        DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, once, notNode, since, implies, always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:1000]{q}) -> ((not{p}) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 1000};
-        DiscreteNode notNode{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since{empty(holder), false, NodeType::SINCE, 3, 0, 0, B_INFINITY};
-        DiscreteNode implies{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0};
-        DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, once, notNode, since, implies, always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AbsentBQR: historically({r} && !{q} && once{q}) -> ((not{p}) since[A:B] {q})
-    else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[3:10] {q})") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 7, 0, 3, 10};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0};
-        DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[30:100] {q})") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 7, 0, 30, 100};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0};
-        DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[300:1000] {q})") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 7, 0, 300, 1000};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0};
-        DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AbsentBR: historically({r} -> (historically[:N](not{p})))
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:10](not{p})))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 3, 0, 10};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_p, inner_always, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:100](not{p})))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 3, 0, 100};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_p, inner_always, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:1000](not{p})))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 3, 0, 1000};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 4, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_p, inner_always, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AlwaysAQ: historically((once[:N]{q}) -> ({p} since {q}))
-    else if (strcmp(arguments.spec, "historically((once[:10]{q}) -> ({p} since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 10};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 0, B_INFINITY};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 3, 4, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, once_q, since_node, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:100]{q}) -> ({p} since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 100};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 0, B_INFINITY};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 3, 4, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, once_q, since_node, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:1000]{q}) -> ({p} since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 1000};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 0, B_INFINITY};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 3, 4, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, once_q, since_node, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AlwaysBQR: historically(({r} && !{q} && once{q}) -> ({p} since[A:B] {q}))
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[3:10] {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 3, 10};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0};
-        DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[30:100] {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 30, 100};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0};
-        DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[300:1000] {q}))") == 0)
+    std::ifstream props_in(args.properties_file);
+    if (!props_in.is_open())
     {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode not_p{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 1, 0, 300, 1000};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 8, 0, 0};
-        DiscreteNode always_node{empty(holder), false, NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        std::cerr << "Error opening properties file: " << args.properties_file << std::endl;
+        exit(1);
     }
-    // AlwaysBR: historically({r} -> (historically[:N]{p}))
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:10]{p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, 10};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 3, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 4, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, inner_always, implies_node, root_always};
 
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:100]{p}))") == 0)
+    std::vector<std::string> formulas;
+    std::string line;
+    while (std::getline(props_in, line))
     {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, 100};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 3, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 4, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, inner_always, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:1000]{p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode inner_always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, 1000};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 2, 3, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 4, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, inner_always, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // RecurBQR: historically(({r} && !{q} && once{q}) -> ((once[:N]({p} or {q})) since {q}))
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:10]({p} or {q})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode p_or_q{empty(holder), false, NodeType::OR, 1, 0, 0, 0};
-        DiscreteNode once_p_or_q{empty(holder), false, NodeType::EVENTUALLY, 0, 7, 0, 10};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 8, 0, 0, B_INFINITY};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 9, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 10, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:100]({p} or {q})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode p_or_q{empty(holder), false, NodeType::OR, 1, 0, 0, 0};
-        DiscreteNode once_p_or_q{empty(holder), false, NodeType::EVENTUALLY, 0, 7, 0, 100};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 8, 0, 0, B_INFINITY};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 9, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 10, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        size_t first = line.find_first_not_of(" \t\r\n");
+        if (first == std::string::npos) continue;
+        formulas.push_back(line);
     }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:1000]({p} or {q})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and1{empty(holder), false, NodeType::AND, 2, 3, 0, 0};
-        DiscreteNode and2{empty(holder), false, NodeType::AND, 5, 4, 0, 0};
-        DiscreteNode p_or_q{empty(holder), false, NodeType::OR, 1, 0, 0, 0};
-        DiscreteNode once_p_or_q{empty(holder), false, NodeType::EVENTUALLY, 0, 7, 0, 1000};
-        DiscreteNode since_node{empty(holder), false, NodeType::SINCE, 8, 0, 0, B_INFINITY};
-        DiscreteNode implies_node{empty(holder), false, NodeType::IMPLIES, 6, 9, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 10, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always};
 
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // RecurGLB: historically(once[:N]{p})
-    else if (strcmp(arguments.spec, "historically(once[:10]{p})") == 0)
+    if (formulas.empty())
     {
-        std::vector<bool> propositionInputs(1);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 10};
-        DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{p, once, always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].p;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        std::cerr << "No formulas found in properties file." << std::endl;
+        exit(1);
     }
-    else if (strcmp(arguments.spec, "historically(once[:100]{p})") == 0)
-    {
-        std::vector<bool> propositionInputs(1);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 100};
-        DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{p, once, always};
 
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].p;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(once[:1000]{p})") == 0)
-    {
-        std::vector<bool> propositionInputs(1);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode once{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, 1000};
-        DiscreteNode always{empty(holder), false, NodeType::ALWAYS, 0, 1, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{p, once, always};
+    DenseMultiPropertyMonitor monitor = createDenseMultiPropertyMonitor(3000);
+    ptl_parser parser;
 
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].p;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // RespondBQR: historically(({r} && !{q} && once{q}) -> ( (({s} -> once[A:B]{p}) and not((not {s}) since[B:] {p})) since {q}))
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[3:10]{p}) and not((not {s}) since[10:] {p})) since {q}))") == 0)
+    for (const auto &f : formulas)
     {
-        std::vector<bool> propositionInputs(4);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 3, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and_A1{empty(holder), false, NodeType::AND, 3, 4, 0, 0};
-        DiscreteNode and_A2{empty(holder), false, NodeType::AND, 6, 5, 0, 0};
-        DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 1, 3, 10};
-        DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 2, 8, 0, 0};
-        DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 2, 0, 0};
-        DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 10, 1, 10, B_INFINITY};
-        DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 11, 0, 0};
-        DiscreteNode and_C{empty(holder), false, NodeType::AND, 9, 12, 0, 0};
-        DiscreteNode since_B{empty(holder), false, NodeType::SINCE, 13, 0, 0, B_INFINITY};
-        DiscreteNode implies_main{empty(holder), false, NodeType::IMPLIES, 7, 14, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 15, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].s;
-            propositionInputs[3] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
+        try {
+            parser.parse_dense(f, monitor);
+        } catch (const std::exception &e) {
+            std::cerr << "Error parsing formula: " << f << "\n" << e.what() << std::endl;
+            exit(1);
         }
-        destroyHolder(holder);
     }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[30:100]{p}) and not((not {s}) since[100:] {p})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(4);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 3, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and_A1{empty(holder), false, NodeType::AND, 3, 4, 0, 0};
-        DiscreteNode and_A2{empty(holder), false, NodeType::AND, 6, 5, 0, 0};
-        DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 1, 30, 100};
-        DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 2, 8, 0, 0};
-        DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 2, 0, 0};
-        DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 10, 1, 100, B_INFINITY};
-        DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 11, 0, 0};
-        DiscreteNode and_C{empty(holder), false, NodeType::AND, 9, 12, 0, 0};
-        DiscreteNode since_B{empty(holder), false, NodeType::SINCE, 13, 0, 0, B_INFINITY};
-        DiscreteNode implies_main{empty(holder), false, NodeType::IMPLIES, 7, 14, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 15, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always};
+    finalize_monitor(monitor);
 
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].s;
-            propositionInputs[3] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[300:1000]{p}) and not((not {s}) since[1000:] {p})) since {q}))") == 0)
+    auto *feeder = create_dense_json_feeder(monitor, args.trace_file);
+    if (!feeder)
     {
-        std::vector<bool> propositionInputs(4);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode q{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 2, 0, 0, 0};
-        DiscreteNode r{empty(holder), false, NodeType::PROPOSITION, 3, 0, 0, 0};
-        DiscreteNode not_q{empty(holder), false, NodeType::NOT, 0, 0, 0, 0};
-        DiscreteNode once_q{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DiscreteNode and_A1{empty(holder), false, NodeType::AND, 3, 4, 0, 0};
-        DiscreteNode and_A2{empty(holder), false, NodeType::AND, 6, 5, 0, 0};
-        DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 1, 300, 1000};
-        DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 2, 8, 0, 0};
-        DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 2, 0, 0};
-        DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 10, 1, 1000, B_INFINITY};
-        DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 11, 0, 0};
-        DiscreteNode and_C{empty(holder), false, NodeType::AND, 9, 12, 0, 0};
-        DiscreteNode since_B{empty(holder), false, NodeType::SINCE, 13, 0, 0, B_INFINITY};
-        DiscreteNode implies_main{empty(holder), false, NodeType::IMPLIES, 7, 14, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 15, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].q;
-            propositionInputs[1] = allInputs[i].p;
-            propositionInputs[2] = allInputs[i].s;
-            propositionInputs[3] = allInputs[i].r;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        std::cerr << "Error creating feeder for trace file: " << args.trace_file << std::endl;
+        exit(1);
     }
-    // RespondGLB: historically(({s} -> once[A:B]{p}) and not((not {s}) since[B:] {p}))
-    else if (strcmp(arguments.spec, "historically(({s} -> once[3:10]{p}) and not((not {s}) since[10:] {p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 3, 10};
-        DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 1, 2, 0, 0};
-        DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 4, 0, 10, B_INFINITY};
-        DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 5, 0, 0};
-        DiscreteNode and_C{empty(holder), false, NodeType::AND, 3, 6, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 7, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always};
 
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].p;
-            propositionInputs[1] = allInputs[i].s;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({s} -> once[30:100]{p}) and not((not {s}) since[100:] {p}))") == 0)
+    std::vector<IntervalSet> output;
+    while (feed_next(feeder, output))
     {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 30, 100};
-        DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 1, 2, 0, 0};
-        DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 4, 0, 100, B_INFINITY};
-        DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 5, 0, 0};
-        DiscreteNode and_C{empty(holder), false, NodeType::AND, 3, 6, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 7, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always};
-
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].p;
-            propositionInputs[1] = allInputs[i].s;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
     }
-    else if (strcmp(arguments.spec, "historically(({s} -> once[300:1000]{p}) and not((not {s}) since[1000:] {p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DiscreteNode p{empty(holder), false, NodeType::PROPOSITION, 0, 0, 0, 0};
-        DiscreteNode s{empty(holder), false, NodeType::PROPOSITION, 1, 0, 0, 0};
-        DiscreteNode once_p{empty(holder), false, NodeType::EVENTUALLY, 0, 0, 300, 1000};
-        DiscreteNode implies_D{empty(holder), false, NodeType::IMPLIES, 1, 2, 0, 0};
-        DiscreteNode not_s{empty(holder), false, NodeType::NOT, 0, 1, 0, 0};
-        DiscreteNode since_F{empty(holder), false, NodeType::SINCE, 4, 0, 1000, B_INFINITY};
-        DiscreteNode not_F{empty(holder), false, NodeType::NOT, 0, 5, 0, 0};
-        DiscreteNode and_C{empty(holder), false, NodeType::AND, 3, 6, 0, 0};
-        DiscreteNode root_always{empty(holder), false, NodeType::ALWAYS, 0, 7, 0, B_INFINITY};
-        std::vector<DiscreteNode> nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always};
 
-        for (size_t i = 0; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i].p;
-            propositionInputs[1] = allInputs[i].s;
-            run_evaluation(nodes, holder, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else
-    {
-        std::cout << "Error: Can't find code for spec: " << arguments.spec << std::endl;
-    }
+    destroy_feeder(feeder);
 }
 
-
-void dense_case(arguments arguments, std::vector<binary_row_reader::TimescalesInput> allInputs)
+void discrete_case(const arguments &args)
 {
-    // AbsentAQ: historically((once[:N]{q}) -> ((not{p}) since {q}))
-    if (strcmp(arguments.spec, "historically((once[:10]{q}) -> ((not{p}) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 10};
-        DenseNode notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY};
-        DenseNode implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0};
-        DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, once, notNode, since, implies, always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:100]{q}) -> ((not{p}) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 100};
-        DenseNode notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY};
-        DenseNode implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0};
-        DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, once, notNode, since, implies, always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:1000]{q}) -> ((not{p}) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 1000};
-        DenseNode notNode{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since{empty(holder), empty(holder), NodeType::SINCE, 3, 0, 0, B_INFINITY};
-        DenseNode implies{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0};
-        DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, once, notNode, since, implies, always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AbsentBQR: historically({r} && !{q} && once{q}) -> ((not{p}) since[A:B] {q})
-    else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[3:10] {q})") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, 3, 10};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0};
-        DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[30:100] {q})") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, 30, 100};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0};
-        DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} && !{q} && once{q}) -> ((not{p}) since[300:1000] {q})") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 7, 0, 300, 1000};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0};
-        DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AbsentBR: historically({r} -> (historically[:N](not{p})))
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:10](not{p})))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, 10};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_p, inner_always, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:100](not{p})))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, 100};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_p, inner_always, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:1000](not{p})))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 3, 0, 1000};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 4, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_p, inner_always, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AlwaysAQ: historically((once[:N]{q}) -> ({p} since {q}))
-    else if (strcmp(arguments.spec, "historically((once[:10]{q}) -> ({p} since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 10};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, once_q, since_node, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:100]{q}) -> ({p} since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 100};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, once_q, since_node, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically((once[:1000]{q}) -> ({p} since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 1000};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 0, B_INFINITY};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 3, 4, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 5, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, once_q, since_node, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AlwaysBQR: historically(({r} && !{q} && once{q}) -> ({p} since[A:B] {q}))
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[3:10] {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 3, 10};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0};
-        DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[30:100] {q}))") == 0)
+    std::ifstream props_in(args.properties_file);
+    if (!props_in.is_open())
     {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 30, 100};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0};
-        DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ({p} since[300:1000] {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode not_p{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 1, 0, 300, 1000};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 8, 0, 0};
-        DenseNode always_node{empty(holder), empty(holder), NodeType::ALWAYS, 0, 9, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, not_p, since_node, implies_node, always_node};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // AlwaysBR: historically({r} -> (historically[:N]{p}))
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:10]{p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, 10};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, inner_always, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        std::cerr << "Error opening properties file: " << args.properties_file << std::endl;
+        exit(1);
     }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:100]{p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, 100};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, inner_always, implies_node, root_always};
 
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically({r} -> (historically[:1000]{p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode inner_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, 1000};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 2, 3, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 4, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, inner_always, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // RecurBQR: historically(({r} && !{q} && once{q}) -> ((once[:N]({p} or {q})) since {q}))
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:10]({p} or {q})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0};
-        DenseNode once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, 10};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:100]({p} or {q})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0};
-        DenseNode once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, 100};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ((once[:1000]({p} or {q})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(3);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and1{empty(holder), empty(holder), NodeType::AND, 2, 3, 0, 0};
-        DenseNode and2{empty(holder), empty(holder), NodeType::AND, 5, 4, 0, 0};
-        DenseNode p_or_q{empty(holder), empty(holder), NodeType::OR, 1, 0, 0, 0};
-        DenseNode once_p_or_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 7, 0, 1000};
-        DenseNode since_node{empty(holder), empty(holder), NodeType::SINCE, 8, 0, 0, B_INFINITY};
-        DenseNode implies_node{empty(holder), empty(holder), NodeType::IMPLIES, 6, 9, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 10, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, r, not_q, once_q, and1, and2, p_or_q, once_p_or_q, since_node, implies_node, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    // RecurGLB: historically(once[:N]{p})
-    else if (strcmp(arguments.spec, "historically(once[:10]{p})") == 0)
+    std::vector<std::string> formulas;
+    std::string line;
+    while (std::getline(props_in, line))
     {
-        std::vector<bool> propositionInputs(1);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 10};
-        DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{p, once, always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].p;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        size_t first = line.find_first_not_of(" \t\r\n");
+        if (first == std::string::npos) continue;
+        formulas.push_back(line);
     }
-    else if (strcmp(arguments.spec, "historically(once[:100]{p})") == 0)
-    {
-        std::vector<bool> propositionInputs(1);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 100};
-        DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{p, once, always};
 
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].p;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(once[:1000]{p})") == 0)
+    if (formulas.empty())
     {
-        std::vector<bool> propositionInputs(1);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode once{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, 1000};
-        DenseNode always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 1, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{p, once, always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].p;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        std::cerr << "No formulas found in properties file." << std::endl;
+        exit(1);
     }
-    // RespondBQR: historically(({r} && !{q} && once{q}) -> ( (({s} -> once[A:B]{p}) and not((not {s}) since[B:] {p})) since {q}))
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[3:10]{p}) and not((not {s}) since[10:] {p})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(4);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 3, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0};
-        DenseNode and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0};
-        DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, 3, 10};
-        DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0};
-        DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0};
-        DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, 10, B_INFINITY};
-        DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0};
-        DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0};
-        DenseNode since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY};
-        DenseNode implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always};
 
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].s;
-            propositionInputs[3] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[30:100]{p}) and not((not {s}) since[100:] {p})) since {q}))") == 0)
-    {
-        std::vector<bool> propositionInputs(4);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 3, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0};
-        DenseNode and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0};
-        DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, 30, 100};
-        DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0};
-        DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0};
-        DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, 100, B_INFINITY};
-        DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0};
-        DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0};
-        DenseNode since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY};
-        DenseNode implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always};
+    DiscreteMultiPropertyMonitor monitor = createDiscreteMultiPropertyMonitor(3000);
+    ptl_parser parser;
 
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].s;
-            propositionInputs[3] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({r} && !{q} && once{q}) -> ( (({s} -> once[300:1000]{p}) and not((not {s}) since[1000:] {p})) since {q}))") == 0)
+    for (const auto &f : formulas)
     {
-        std::vector<bool> propositionInputs(4);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode q{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 2, 0, 0, 0};
-        DenseNode r{empty(holder), empty(holder), NodeType::PROPOSITION, 3, 0, 0, 0};
-        DenseNode not_q{empty(holder), empty(holder), NodeType::NOT, 0, 0, 0, 0};
-        DenseNode once_q{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 0, B_INFINITY};
-        DenseNode and_A1{empty(holder), empty(holder), NodeType::AND, 3, 4, 0, 0};
-        DenseNode and_A2{empty(holder), empty(holder), NodeType::AND, 6, 5, 0, 0};
-        DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 1, 300, 1000};
-        DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 2, 8, 0, 0};
-        DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 2, 0, 0};
-        DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 10, 1, 1000, B_INFINITY};
-        DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 11, 0, 0};
-        DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 9, 12, 0, 0};
-        DenseNode since_B{empty(holder), empty(holder), NodeType::SINCE, 13, 0, 0, B_INFINITY};
-        DenseNode implies_main{empty(holder), empty(holder), NodeType::IMPLIES, 7, 14, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 15, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{q, p, s, r, not_q, once_q, and_A1, and_A2, once_p, implies_D, not_s, since_F, not_F, and_C, since_B, implies_main, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].q;
-            propositionInputs[1] = allInputs[i - 1].p;
-            propositionInputs[2] = allInputs[i - 1].s;
-            propositionInputs[3] = allInputs[i - 1].r;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
+        try {
+            parser.parse_discrete(f, monitor);
+        } catch (const std::exception &e) {
+            std::cerr << "Error parsing formula: " << f << "\n" << e.what() << std::endl;
+            exit(1);
         }
-        destroyHolder(holder);
     }
-    // RespondGLB: historically(({s} -> once[A:B]{p}) and not((not {s}) since[B:] {p}))
-    else if (strcmp(arguments.spec, "historically(({s} -> once[3:10]{p}) and not((not {s}) since[10:] {p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 3, 10};
-        DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0};
-        DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, 10, B_INFINITY};
-        DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0};
-        DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always};
+    finalize_monitor(monitor);
 
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].p;
-            propositionInputs[1] = allInputs[i - 1].s;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else if (strcmp(arguments.spec, "historically(({s} -> once[30:100]{p}) and not((not {s}) since[100:] {p}))") == 0)
+    auto *feeder = create_discrete_json_feeder(monitor, args.trace_file);
+    if (!feeder)
     {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 30, 100};
-        DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0};
-        DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, 100, B_INFINITY};
-        DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0};
-        DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always};
-
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].p;
-            propositionInputs[1] = allInputs[i - 1].s;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
+        std::cerr << "Error creating feeder for trace file: " << args.trace_file << std::endl;
+        exit(1);
     }
-    else if (strcmp(arguments.spec, "historically(({s} -> once[300:1000]{p}) and not((not {s}) since[1000:] {p}))") == 0)
-    {
-        std::vector<bool> propositionInputs(2);
-        IntervalSetHolder holder = newHolder(1000);
-        DenseNode p{empty(holder), empty(holder), NodeType::PROPOSITION, 0, 0, 0, 0};
-        DenseNode s{empty(holder), empty(holder), NodeType::PROPOSITION, 1, 0, 0, 0};
-        DenseNode once_p{empty(holder), empty(holder), NodeType::EVENTUALLY, 0, 0, 300, 1000};
-        DenseNode implies_D{empty(holder), empty(holder), NodeType::IMPLIES, 1, 2, 0, 0};
-        DenseNode not_s{empty(holder), empty(holder), NodeType::NOT, 0, 1, 0, 0};
-        DenseNode since_F{empty(holder), empty(holder), NodeType::SINCE, 4, 0, 1000, B_INFINITY};
-        DenseNode not_F{empty(holder), empty(holder), NodeType::NOT, 0, 5, 0, 0};
-        DenseNode and_C{empty(holder), empty(holder), NodeType::AND, 3, 6, 0, 0};
-        DenseNode root_always{empty(holder), empty(holder), NodeType::ALWAYS, 0, 7, 0, B_INFINITY};
-        std::vector<DenseNode> nodes{p, s, once_p, implies_D, not_s, since_F, not_F, and_C, root_always};
 
-        for (size_t i = 1; i < allInputs.size(); i++)
-        {
-            propositionInputs[0] = allInputs[i - 1].p;
-            propositionInputs[1] = allInputs[i - 1].s;
-            run_evaluation(nodes, holder, allInputs[i - 1].time, allInputs[i].time, propositionInputs);
-            swapBuffers(holder);
-        }
-        destroyHolder(holder);
-    }
-    else
+    std::vector<bool> output;
+    while (feed_next(feeder, output))
     {
-        std::cout << "Error: Can't find code for spec: " << arguments.spec << std::endl;
     }
 
-}
\ No newline at end of file
+    destroy_feeder(feeder);
+}
diff --git a/tests/test_parse.cpp b/tests/test_parse.cpp
index d9b5a53..93e6747 100644
--- a/tests/test_parse.cpp
+++ b/tests/test_parse.cpp
@@ -24,9 +24,17 @@ static bool trees_equal(const std::vector<DenseNode>& a, int rootA,
     if (na.type == NodeType::NOT || na.type == NodeType::EVENTUALLY || na.type == NodeType::ALWAYS)
         return trees_equal(a, na.rightOperandIndex, b, nb.rightOperandIndex);
 
-    // Binary operators (AND, OR, IMPLIES, SINCE): both children must match
-    return trees_equal(a, na.leftOperandIndex, b, nb.leftOperandIndex)
-        && trees_equal(a, na.rightOperandIndex, b, nb.rightOperandIndex);
+    // Binary operators (IMPLIES, SINCE): both children must match
+    if (na.type == NodeType::IMPLIES || na.type == NodeType::SINCE) {
+        return trees_equal(a, na.leftOperandIndex, b, nb.leftOperandIndex)
+            && trees_equal(a, na.rightOperandIndex, b, nb.rightOperandIndex);
+    }
+    // Commutative Binary operators (AND, OR): both children must match, but order can change.
+    return (trees_equal(a, na.leftOperandIndex, b, nb.leftOperandIndex)
+        && trees_equal(a, na.rightOperandIndex, b, nb.rightOperandIndex))
+        ||
+        (trees_equal(a, na.leftOperandIndex, b, nb.rightOperandIndex)
+        && trees_equal(a, na.rightOperandIndex, b, nb.leftOperandIndex));
 }