Remove CTL quantifiers

boost_tests/CMakeLists.txt

@@ -30,7 +30,7 @@ add_test(NAME XMLPrinterTests COMMAND XMLPrinterTests)
 add_test(NAME PQLParserTests COMMAND PQLParserTests)
 add_test(NAME PredicateCheckerTests COMMAND PredicateCheckerTests)
 add_test(NAME reachability COMMAND reachability)
-add_test(NAME ltl COMMAND reachability)
+add_test(NAME ltl COMMAND ltl)
 add_test(NAME games COMMAND games)
 add_test(NAME color COMMAND color)
 

boost_tests/color_test.cpp

@@ -27,13 +27,14 @@
 
 using namespace PetriEngine;
 using namespace PetriEngine::Colored;
+namespace utf = boost::unit_test;
 
 BOOST_AUTO_TEST_CASE(DirectoryTest) {
     BOOST_REQUIRE(getenv("TEST_FILES"));
 }
 
 
-BOOST_AUTO_TEST_CASE(InitialMarkingMismatch) {
+BOOST_AUTO_TEST_CASE(InitialMarkingMismatch, * utf::timeout(5)) {
 
     std::string model("/models/color_mismatch.pnml");
     std::string query("/models/color_mismatch.xml");
@@ -49,7 +50,7 @@ BOOST_AUTO_TEST_CASE(InitialMarkingMismatch) {
     BOOST_REQUIRE(saw_exception);
 }
 
-BOOST_AUTO_TEST_CASE(InitialMarkingMatch) {
+BOOST_AUTO_TEST_CASE(InitialMarkingMatch, * utf::timeout(5)) {
 
     std::string model("/models/color_match.pnml");
     std::string query("/models/color_match.xml");
@@ -69,7 +70,7 @@ BOOST_AUTO_TEST_CASE(InitialMarkingMatch) {
 }
 
 
-BOOST_AUTO_TEST_CASE(PhilosophersDynCOL03) {
+BOOST_AUTO_TEST_CASE(PhilosophersDynCOL03, * utf::timeout(60)) {
 
     std::string model("/models/PhilosophersDyn-COL-03/model.pnml");
     std::string query("/models/PhilosophersDyn-COL-03/ReachabilityCardinality.xml");
@@ -124,7 +125,7 @@ BOOST_AUTO_TEST_CASE(PhilosophersDynCOL03) {
     }
 }
 
-BOOST_AUTO_TEST_CASE(PetersonCOL2) {
+BOOST_AUTO_TEST_CASE(PetersonCOL2, * utf::timeout(60)) {
 
     std::string model("/models/Peterson-COL-2/model.pnml");
     std::string query("/models/Peterson-COL-2/ReachabilityCardinality.xml");
@@ -188,11 +189,11 @@ BOOST_AUTO_TEST_CASE(PetersonCOL2) {
 }
 
 
-BOOST_AUTO_TEST_CASE(UtilityControlRoomCOLZ2T3N04) {
+BOOST_AUTO_TEST_CASE(UtilityControlRoomCOLZ2T3N04, * utf::timeout(60)) {
 
     std::string model("/models/UtilityControlRoom-COL-Z2T3N04/model.pnml");
     std::string query("/models/UtilityControlRoom-COL-Z2T3N04/ReachabilityCardinality.xml");
-    // this model is to large to verify as a test, but unfolding should be ok.
+    // this model is to large too verify as a test, but unfolding should be ok.
     // the unfolding provoked an error in the CFP of colored nets.
     std::set<size_t> qnums{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
     for(auto partition : {false, true})
@@ -219,11 +220,11 @@ BOOST_AUTO_TEST_CASE(UtilityControlRoomCOLZ2T3N04) {
     }
 }
 
-BOOST_AUTO_TEST_CASE(NeoElectionCOL3) {
+BOOST_AUTO_TEST_CASE(NeoElectionCOL3, * utf::timeout(60)) {
 
     std::string model("/models/NeoElection-COL-3/model.pnml");
     std::string query("/models/NeoElection-COL-3/ReachabilityCardinality.xml");
-    // this model is to large to verify as a test, but unfolding should be ok.
+    // this model is to large too verify as a test, but unfolding should be ok.
     // the unfolding provoked an error in the CFP of colored nets.
     std::set<size_t> qnums{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
     for(auto partition : {false, true})

boost_tests/game_test.cpp

@@ -26,6 +26,7 @@
 
 using namespace PetriEngine;
 using namespace PetriEngine::Synthesis;
+namespace utf = boost::unit_test;
 
 BOOST_AUTO_TEST_CASE(DirectoryTest) {
     BOOST_REQUIRE(getenv("TEST_FILES"));
@@ -56,7 +57,7 @@ void test_single_game(const char* fn, Reachability::ResultPrinter::Result expect
 }
 
 
-BOOST_AUTO_TEST_CASE(Algorithm1Counterexample) {
+BOOST_AUTO_TEST_CASE(Algorithm1Counterexample, * utf::timeout(5)) {
     std::cerr << "Q1" << std::endl;
     test_single_game("algorithm 1 counterexample", Reachability::ResultPrinter::NotSatisfied, 0);
     std::cerr << "Q2" << std::endl;
@@ -67,43 +68,43 @@ BOOST_AUTO_TEST_CASE(Algorithm1Counterexample) {
     test_single_game("algorithm 1 counterexample", Reachability::ResultPrinter::Satisfied, 3);
 }
 
-BOOST_AUTO_TEST_CASE(Algorithm1Counterexample2) {
+BOOST_AUTO_TEST_CASE(Algorithm1Counterexample2, * utf::timeout(5)) {
     test_single_game("algorithm 1 counterexample 2", Reachability::ResultPrinter::Satisfied);
 }
 
-BOOST_AUTO_TEST_CASE(CycleTestFalse) {
+BOOST_AUTO_TEST_CASE(CycleTestFalse, * utf::timeout(5)) {
     test_single_game("cycle test false", Reachability::ResultPrinter::Satisfied);
 }
 
-BOOST_AUTO_TEST_CASE(CycleTestTrue2) {
+BOOST_AUTO_TEST_CASE(CycleTestTrue2, * utf::timeout(5)) {
     test_single_game("cycle test true 2", Reachability::ResultPrinter::Satisfied);
 }
 
-BOOST_AUTO_TEST_CASE(CycleTestTrue3) {
+BOOST_AUTO_TEST_CASE(CycleTestTrue3, * utf::timeout(5)) {
     test_single_game("cycle test true 3", Reachability::ResultPrinter::Satisfied);
 }
 
 
-BOOST_AUTO_TEST_CASE(Player2LessReduction) {
+BOOST_AUTO_TEST_CASE(Player2LessReduction, * utf::timeout(5)) {
     test_single_game("player 2 less reduction", Reachability::ResultPrinter::NotSatisfied);
 }
 
-BOOST_AUTO_TEST_CASE(Player2) {
+BOOST_AUTO_TEST_CASE(Player2, * utf::timeout(5)) {
     test_single_game("player 2", Reachability::ResultPrinter::Satisfied);
 }
 
-BOOST_AUTO_TEST_CASE(SafeTest) {
+BOOST_AUTO_TEST_CASE(SafeTest, * utf::timeout(5)) {
     test_single_game("safe test", Reachability::ResultPrinter::Satisfied);
 }
 
-BOOST_AUTO_TEST_CASE(UnsafeTest) {
+BOOST_AUTO_TEST_CASE(UnsafeTest, * utf::timeout(5)) {
     test_single_game("unsafe test", Reachability::ResultPrinter::Satisfied);
 }
 
-BOOST_AUTO_TEST_CASE(AGPorFail) {
+BOOST_AUTO_TEST_CASE(AGPorFail, * utf::timeout(5)) {
     test_single_game("AG_por_fail", Reachability::ResultPrinter::NotSatisfied);
 }
 
-BOOST_AUTO_TEST_CASE(GenModel0PorSuccFail) {
+BOOST_AUTO_TEST_CASE(GenModel0PorSuccFail, * utf::timeout(5)) {
     test_single_game("gen_model_0", Reachability::ResultPrinter::NotSatisfied);
 }

boost_tests/ltl_test.cpp

@@ -27,13 +27,14 @@
 
 using namespace PetriEngine;
 using namespace PetriEngine::Colored;
+namespace utf = boost::unit_test;
 
 BOOST_AUTO_TEST_CASE(DirectoryTest) {
     BOOST_REQUIRE(getenv("TEST_FILES"));
 }
 
 
-BOOST_AUTO_TEST_CASE(AngiogenesisPT01LTLCardinality) {
+BOOST_AUTO_TEST_CASE(AngiogenesisPT01LTLCardinality, * utf::timeout(300)) {
 
     std::set<size_t> qnums{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
     std::vector<Reachability::ResultPrinter::Result> expected{
@@ -85,7 +86,7 @@ BOOST_AUTO_TEST_CASE(AngiogenesisPT01LTLCardinality) {
     }
 }
 
-BOOST_AUTO_TEST_CASE(AngiogenesisPT01ReachabilityFireability) {
+BOOST_AUTO_TEST_CASE(AngiogenesisPT01ReachabilityFireability, * utf::timeout(300)) {
 
     std::set<size_t> qnums{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
     std::vector<Reachability::ResultPrinter::Result> expected{

boost_tests/reachability_test.cpp

@@ -25,12 +25,13 @@
 
 using namespace PetriEngine;
 using namespace PetriEngine::Colored;
+namespace utf = boost::unit_test;
 
 BOOST_AUTO_TEST_CASE(DirectoryTest) {
     BOOST_REQUIRE(getenv("TEST_FILES"));
 }
 
-BOOST_AUTO_TEST_CASE(AngiogenesisPT01ReachabilityCardinality) {
+BOOST_AUTO_TEST_CASE(AngiogenesisPT01ReachabilityCardinality, * utf::timeout(60)) {
 
     std::set<size_t> qnums{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
     std::vector<Reachability::ResultPrinter::Result> expected{
@@ -72,7 +73,7 @@ BOOST_AUTO_TEST_CASE(AngiogenesisPT01ReachabilityCardinality) {
     }
 }
 
-BOOST_AUTO_TEST_CASE(AngiogenesisPT01ReachabilityFireability) {
+BOOST_AUTO_TEST_CASE(AngiogenesisPT01ReachabilityFireability, * utf::timeout(60)) {
 
     std::set<size_t> qnums{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15};
     std::vector<Reachability::ResultPrinter::Result> expected{

include/LTL/Algorithm/ModelChecker.h

@@ -61,7 +61,7 @@ namespace LTL {
         virtual ~ModelChecker() = default;
 
         [[nodiscard]] bool is_weak() const {
-            return _is_weak;
+            return _shortcircuitweak;
         }
 
         size_t get_explored() {
@@ -96,18 +96,11 @@ namespace LTL {
                     << "\tmax tokens:        " << max_tokens << std::endl;
         }
 
-        virtual void print_stats(std::ostream &os, const LTL::Structures::ProductStateSetInterface &stateSet) const {
-            print_stats(os, stateSet.discovered(), stateSet.max_tokens());
-        }
-
-
         const PetriEngine::PetriNet& _net;
         PetriEngine::PQL::Condition_ptr _formula;
         Structures::ProductStateFactory _factory;
         const Structures::BuchiAutomaton& _buchi;
         bool _shortcircuitweak;
-        bool _weakskip = false;
-        bool _is_weak = false;
         bool _build_trace = false;
         Heuristic* _heuristic = nullptr;
         size_t _loop = std::numeric_limits<size_t>::max();

include/LTL/Algorithm/NestedDepthFirstSearch.h

@@ -25,6 +25,8 @@
 #include "utils/structures/light_deque.h"
 #include "LTL/Structures/ProductStateFactory.h"
 
+#include <ptrie/ptrie_map.h>
+
 namespace LTL {
 
     /**
@@ -55,9 +57,9 @@ namespace LTL {
         using State = LTL::Structures::ProductState;
         std::pair<bool,size_t> mark(State& state, uint8_t);
 
-        LTL::Structures::BitProductStateSet<> _states;
+        LTL::Structures::BitProductStateSet<ptrie::map<Structures::stateid_t, uint8_t>> _states;
 
-        std::unordered_map<size_t, uint8_t> _markers;
+        ptrie::map<size_t, uint8_t> _markers;
         static constexpr uint8_t MARKER1 = 1;
         static constexpr uint8_t MARKER2 = 2;
         size_t _mark_count[3] = {0,0,0};

include/LTL/Algorithm/TarjanModelChecker.h

@@ -24,10 +24,11 @@
 #include "LTL/Structures/BitProductStateSet.h"
 #include "LTL/SuccessorGeneration/ResumingSuccessorGenerator.h"
 #include "LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h"
+#include "utils/structures/light_deque.h"
+
+#include <ptrie/ptrie.h>
 
 #include <limits>
-#include <stack>
-#include <unordered_set>
 
 namespace LTL {
 
@@ -49,8 +50,8 @@ namespace LTL {
                            uint32_t kbound)
                 : ModelChecker(net, cond, buchi), _k_bound(kbound)
         {
-            if (buchi.buchi().num_states() > 65535) {
-                throw base_error("Cannot handle Büchi automata larger than 2^16 states");
+            if (buchi.buchi().num_states() > 1048576) {
+                throw base_error("Cannot handle Büchi automata larger than 2^20 states");
             }
             _chash.fill(std::numeric_limits<idx_t>::max());
         }
@@ -77,16 +78,16 @@ namespace LTL {
         // 64 MB hash table
         static constexpr idx_t _hash_sz = 16777216;
 
-        std::unordered_set<idx_t> _store;
+        ptrie::set<idx_t,17,32,8> _store;
 
         // rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack
         // corresponding to state. Collisions are resolved using linked list via CEntry::next.
         std::array<idx_t, _hash_sz> _chash;
         static_assert(sizeof(_chash) == (1U << 27U));
 
-        static inline idx_t hash(idx_t id)
+        static inline idx_t hash(idx_t buchi_state, idx_t marking_id)
         {
-            return id % _hash_sz;
+            return (buchi_state xor marking_id) % _hash_sz;
         }
 
         struct plain_centry_t {
@@ -114,7 +115,7 @@ namespace LTL {
 
 
         // cstack positions of accepting states in current search path, for quick access.
-        std::stack<idx_t> _astack;
+        light_deque<idx_t> _astack;
 
         bool _invariant_loop = true;
         size_t _loop_state = std::numeric_limits<size_t>::max();
@@ -125,23 +126,23 @@ namespace LTL {
         LTLPartialOrder _order = LTLPartialOrder::None;
 
         // TODO, instead of this template hell, we should really just have a templated state that we shuffle around.
-        template<typename T, typename D, typename S>
-        void push(std::vector<T>& cstack, std::stack<D>& dstack, S& successor_generator, State &state, size_t stateid);
+        template<typename StateSet, typename T, typename D, typename S>
+        void push(StateSet& s, light_deque<T>& cstack, light_deque<D>& dstack, S& successor_generator, State &state, size_t stateid);
 
         template<typename S, typename T, typename D, typename SuccGen>
-        void pop(S& seen, std::vector<T>& cstack, std::stack<D>& dstack, SuccGen& successorGenerator);
+        void pop(S& seen, light_deque<T>& cstack, light_deque<D>& dstack, SuccGen& successorGenerator);
 
         template<typename T, typename D, typename SuccGen>
-        void update(std::vector<T>& cstack, std::stack<D>& d, SuccGen& successorGenerator, idx_t to);
+        void update(light_deque<T>& cstack, light_deque<D>& d, SuccGen& successorGenerator, idx_t to);
 
         template<typename S, typename T, typename SuccGen, typename D>
-        bool next_trans(S& seen, std::vector<T>& cstack, SuccGen& successorGenerator, State &state, State &parent, D &delem);
+        bool next_trans(S& seen, light_deque<T>& cstack, SuccGen& successorGenerator, State &state, State &parent, D &delem);
 
-        template<typename T>
-        void popCStack(std::vector<T>& cstack);
+        template<typename StateSet, typename T>
+        void popCStack(StateSet& s, light_deque<T>& cstack);
 
         template<typename S, typename D, typename C>
-        void build_trace(S& seen, std::stack<D> &&dstack, std::vector<C>& cstack);
+        void build_trace(S& seen, light_deque<D> &&dstack, light_deque<C>& cstack);
     };
 }
 

include/LTL/LTLToBuchi.h

@@ -87,22 +87,6 @@ namespace LTL {
 
         void _accept(const PetriEngine::PQL::CompareConjunction *element) override;
 
-        void _accept(const PetriEngine::PQL::EFCondition *condition) override;
-
-        void _accept(const PetriEngine::PQL::EGCondition *condition) override;
-
-        void _accept(const PetriEngine::PQL::AGCondition *condition)  override;
-
-        void _accept(const PetriEngine::PQL::AFCondition *condition)  override;
-
-        void _accept(const PetriEngine::PQL::EXCondition *condition) override;
-
-        void _accept(const PetriEngine::PQL::AXCondition *condition) override;
-
-        void _accept(const PetriEngine::PQL::EUCondition *condition) override;
-
-        void _accept(const PetriEngine::PQL::AUCondition *condition) override;
-
         void _accept(const PetriEngine::PQL::GCondition *condition)  override;
 
         void _accept(const PetriEngine::PQL::FCondition *condition) override;
@@ -111,6 +95,8 @@ namespace LTL {
 
         void _accept(const PetriEngine::PQL::UntilCondition *condition) override;
 
+        void _accept(const PetriEngine::PQL::ReleaseCondition *condition) override;
+
     public:
 
         explicit FormulaToSpotSyntax(APCompression compress_aps = APCompression::Choose)