Merge pull request #26 from DEIS-Tools/renaming_constraints

Renaming constraints
DEIS-Tools · Jul 19, 2023 · e300241 · e300241
2 parents b5aafec + 86c11ec
commit e300241
Show file tree

Hide file tree

Showing 18 changed files with 314 additions and 132 deletions.
diff --git a/.github/workflows/build-linux-clang.yml b/.github/workflows/build-linux-clang.yml
@@ -26,13 +26,13 @@ jobs:
         run: |
           mkdir -p build
           cd build
-          CC=clang CXX=clang++ cmake ../ -DCMAKE_BUILD_TYPE=Prebuild -DBUILD_TESTING=ON  ..
+          CC=clang CXX=clang++ cmake ../ -DCMAKE_BUILD_TYPE=Prebuild -DPARDIBAAL_BuildTests=ON  ..
           make
       - name: Build
         run: |
           mkdir -p build
           cd build
-          CC=clang CXX=clang++ cmake ../ -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON  ..
+          CC=clang CXX=clang++ cmake ../ -DCMAKE_BUILD_TYPE=Debug -DPARDIBAAL_BuildTests=ON  ..
           make
       - name: Test
         run: |

diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml
@@ -25,13 +25,13 @@ jobs:
         run: |
           mkdir -p build
           cd build
-          CC=gcc-10 CXX=g++-10 cmake ../ -DCMAKE_BUILD_TYPE=Prebuild -DDBM_BuildTests=ON -DBUILD_TESTING=ON  ..
+          CC=gcc-10 CXX=g++-10 cmake ../ -DCMAKE_BUILD_TYPE=Prebuild -DPARDIBAAL_BuildTests=ON  ..
           make
       - name: Build
         run: |
           mkdir -p build
           cd build
-          CC=gcc-10 CXX=g++-10 cmake ../ -DCMAKE_BUILD_TYPE=Debug -DDBM_BuildTests=ON -DBUILD_TESTING=ON  ..
+          CC=gcc-10 CXX=g++-10 cmake ../ -DCMAKE_BUILD_TYPE=Debug -DPARDIBAAL_BuildTests=ON  ..
           make
       - name: Test
         run: |

diff --git a/.github/workflows/build-macos.yml b/.github/workflows/build-macos.yml
@@ -25,7 +25,7 @@ jobs:
         run: |
           mkdir -p build
           cd build
-          CC=clang CXX=clang++ cmake ../ -DCMAKE_BUILD_TYPE=Debug -DBUILD_TESTING=ON -DPARDIBAAL_GetDependencies=OFF ..
+          CC=clang CXX=clang++ cmake ../ -DCMAKE_BUILD_TYPE=Debug -DPARDIBAAL_BuildTests=ON -DPARDIBAAL_GetDependencies=OFF ..
           make
       - name: Test
         run: |

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -9,7 +9,7 @@ if (NOT CMAKE_BUILD_TYPE)
     set(CMAKE_BUILD_TYPE Debug)
 endif (NOT CMAKE_BUILD_TYPE)
 
-option(PARDIBAAL_BuildTests "Build the unit tests when BUILD_TESTING is enabled." ON)
+option(PARDIBAAL_BuildTests "Build the unit tests." OFF)
 option(PARDIBAAL_GetDependencies "Fetch external dependencies from web." ON)
 
 if (PARDIBAAL_BuildTests)
@@ -51,7 +51,7 @@ if (PARDIBAAL_GetDependencies)
         set(BOOST_CONFIG_JAM "using gcc : : ${CMAKE_CXX_COMPILER}")
     endif ()
 
-    if(BUILD_TESTING AND PARDIBAAL_BuildTests)
+    if(PARDIBAAL_BuildTests)
         ExternalProject_Add(
             boost-ext
             URL https://boostorg.jfrog.io/artifactory/main/release/1.78.0/source/boost_1_78_0.zip
@@ -73,7 +73,7 @@ if(NOT CMAKE_BUILD_TYPE MATCHES Prebuild)
     include_directories(include)
     add_subdirectory(src)
 endif()
-if(BUILD_TESTING AND PARDIBAAL_BuildTests)
+if(PARDIBAAL_BuildTests)
     if (CMAKE_BUILD_TYPE MATCHES Prebuild)
         # dummy for pre-build
         add_custom_target( prebuild )

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -3,15 +3,15 @@ set(HEADER_FILES
         pardibaal/DBM.h
         pardibaal/bounds_table_t.h
         pardibaal/bound_t.h
-        pardibaal/clock_constraint_t.h)
+        pardibaal/difference_bound_t.h)
 
 add_library(pardibaal
         ${HEADER_FILES}
         pardibaal/Federation.cpp
         pardibaal/DBM.cpp
         pardibaal/bounds_table_t.cpp
         pardibaal/bound_t.cpp
-        pardibaal/clock_constraint_t.cpp)
+        pardibaal/difference_bound_t.cpp)
 
 target_include_directories (pardibaal PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
 

diff --git a/src/pardibaal/DBM.cpp b/src/pardibaal/DBM.cpp
@@ -36,6 +36,8 @@ namespace pardibaal {
     relation_t relation_t::superset() {return relation_t(false, false, true, false);}
     relation_t relation_t::different() {return relation_t(false, false, false, true);}
 
+    relation_e relation_t::type() const {return is_equal() ? EQUAL : is_subset() ? SUBSET : is_superset() ? SUPERSET : DIFFERENT;}
+
     bool relation_t::is_equal() const {return _is_equal;}
     bool relation_t::is_subset() const {return _is_subset;}
     bool relation_t::is_superset() const {return _is_superset;}
@@ -57,7 +59,7 @@ namespace pardibaal {
 
     void DBM::set(dim_t i, dim_t j, bound_t bound) {this->_bounds_table.set(i, j, bound);}
 
-    void DBM::set(const clock_constraint_t& constraint) {
+    void DBM::set(const difference_bound_t& constraint) {
         this->_bounds_table.set(constraint._i, constraint._j, constraint._bound);
     }
 
@@ -68,7 +70,7 @@ namespace pardibaal {
             this->set(0, 0, bound_t::non_strict(-1));
     }
 
-    void DBM::subtract(clock_constraint_t constraint) {
+    void DBM::subtract(difference_bound_t constraint) {
         this->subtract(constraint._i, constraint._j, constraint._bound);
     }
 
@@ -93,15 +95,16 @@ namespace pardibaal {
     }
 
     bool DBM::is_satisfying(dim_t x, dim_t y, bound_t g) const {
+        if (this->is_empty()) return false;
         return bound_t::zero() <= (this->_bounds_table.at(y, x) + g);
     }
 
-    bool DBM::is_satisfying(const clock_constraint_t& constraint) const {
+    bool DBM::is_satisfying(const difference_bound_t& constraint) const {
         return is_satisfying(constraint._i, constraint._j, constraint._bound);
     }
 
-    bool DBM::is_satisfying(const std::vector<clock_constraint_t>& constraints) const {
-        return std::all_of(constraints.begin(), constraints.end(), [this](const clock_constraint_t& c) {
+    bool DBM::is_satisfying(const std::vector<difference_bound_t>& constraints) const {
+        return std::all_of(constraints.begin(), constraints.end(), [this](const difference_bound_t& c) {
             return this->is_satisfying(c);
         });
     }
@@ -201,7 +204,7 @@ namespace pardibaal {
     }
 
     bool DBM::is_intersecting(const Federation& fed) const {
-        return fed.intersects(*this);
+        return fed.is_intersecting(*this);
     }
 
     bool DBM::is_unbounded() const {
@@ -278,11 +281,11 @@ namespace pardibaal {
         }
     }
 
-    void DBM::restrict(const clock_constraint_t& constraint) {
+    void DBM::restrict(const difference_bound_t& constraint) {
         restrict(constraint._i, constraint._j, constraint._bound);
     }
 
-    void DBM::restrict(const std::vector<clock_constraint_t> &constraints) {
+    void DBM::restrict(const std::vector<difference_bound_t> &constraints) {
         for (const auto& c : constraints)
             this->restrict(c);
     }

diff --git a/src/pardibaal/DBM.h b/src/pardibaal/DBM.h
@@ -28,10 +28,12 @@
 
 #include "bound_t.h"
 #include "bounds_table_t.h"
-#include "clock_constraint_t.h"
+#include "difference_bound_t.h"
 
 namespace pardibaal {
     class Federation;
+
+    enum relation_e {EQUAL, SUBSET, SUPERSET, DIFFERENT};
     /** 
      * Relation struct
      * represents the relation between two DBMs.
@@ -51,6 +53,8 @@ namespace pardibaal {
         [[nodiscard]] static relation_t superset();
         [[nodiscard]] static relation_t different();
 
+        [[nodiscard]] relation_e type() const;
+
         [[nodiscard]] bool is_equal() const;
         [[nodiscard]] bool is_subset() const;
         [[nodiscard]] bool is_superset() const;
@@ -69,18 +73,18 @@ namespace pardibaal {
 
         [[nodiscard]] bound_t at(dim_t i, dim_t j) const;
         void set(dim_t i, dim_t j, bound_t bound);
-        void set(const clock_constraint_t& constraint);
+        void set(const difference_bound_t& constraint);
 
         void subtract(dim_t i, dim_t j, bound_t bound);
-        void subtract(clock_constraint_t constraint);
+        void subtract(difference_bound_t constraint);
 
         [[nodiscard]] dim_t dimension() const;
 
         [[nodiscard]] bool is_empty() const;
 
         [[nodiscard]] bool is_satisfying(dim_t x, dim_t y, bound_t g) const;
-        [[nodiscard]] bool is_satisfying(const clock_constraint_t& constraint) const;
-        [[nodiscard]] bool is_satisfying(const std::vector<clock_constraint_t>& constraints) const;
+        [[nodiscard]] bool is_satisfying(const difference_bound_t& constraint) const;
+        [[nodiscard]] bool is_satisfying(const std::vector<difference_bound_t>& constraints) const;
 
         /**
          * Relation between this dbm and another dbm.
@@ -184,8 +188,8 @@ namespace pardibaal {
         void interval_delay(val_t lower, val_t upper);
 
         void restrict(dim_t x, dim_t y, bound_t g);
-        void restrict(const clock_constraint_t& constraint);
-        void restrict(const std::vector<clock_constraint_t>& constraints);
+        void restrict(const difference_bound_t& constraint);
+        void restrict(const std::vector<difference_bound_t>& constraints);
         void free(dim_t x);
         void assign(dim_t x, val_t m);
         void copy(dim_t x, dim_t y);

diff --git a/src/pardibaal/Federation.cpp b/src/pardibaal/Federation.cpp
@@ -73,6 +73,16 @@ namespace pardibaal {
             this->add(dbm);
     }
 
+    void Federation::subtract(dim_t i, dim_t j, bound_t bound) {
+        for (auto& z : zones) {
+            z.subtract(i, j, bound);
+        }
+    }
+
+    void Federation::subtract(difference_bound_t constraint) {
+        this->subtract(constraint._i, constraint._j, constraint._bound);
+    }
+
     void Federation::subtract(const DBM& dbm) {
 #ifndef NEXCEPTIONS
         if (!zones.empty()) {
@@ -133,11 +143,11 @@ namespace pardibaal {
         return false;
     }
 
-    bool Federation::is_satisfying(const clock_constraint_t& constraint) const {
+    bool Federation::is_satisfying(const difference_bound_t& constraint) const {
         return is_satisfying(constraint._i, constraint._j, constraint._bound);
     }
 
-    bool Federation::is_satisfying(const std::vector<clock_constraint_t>& constraints) const {
+    bool Federation::is_satisfying(const std::vector<difference_bound_t>& constraints) const {
         for (const auto& c : constraints)
             if (not is_satisfying(c._i, c._j, c._bound))
                 return false;
@@ -298,12 +308,12 @@ namespace pardibaal {
     template bool Federation::is_superset<false>(const Federation& fed) const;
 
 
-    bool Federation::intersects(const DBM& dbm) const {
+    bool Federation::is_intersecting(const DBM& dbm) const {
         return std::any_of(this->begin(), this->end(), [&dbm](const DBM& z){return z.is_intersecting(dbm);});
     }
 
-    bool Federation::intersects(const Federation& fed) const {
-        return std::any_of(fed.begin(), fed.end(), [this](const DBM& dbm){return this->intersects(dbm);});
+    bool Federation::is_intersecting(const Federation& fed) const {
+        return std::any_of(fed.begin(), fed.end(), [this](const DBM& dbm){return this->is_intersecting(dbm);});
     }
 
     bool Federation::is_unbounded() const {
@@ -339,11 +349,11 @@ namespace pardibaal {
         make_consistent();
     }
 
-    void Federation::restrict(const clock_constraint_t& constraint) {
+    void Federation::restrict(const difference_bound_t& constraint) {
         restrict(constraint._i, constraint._j, constraint._bound);
     }
 
-    void Federation::restrict(const std::vector<clock_constraint_t>& constraints) {
+    void Federation::restrict(const std::vector<difference_bound_t>& constraints) {
         for (DBM& dbm : zones)
             dbm.restrict(constraints);
         make_consistent();

diff --git a/src/pardibaal/Federation.h b/src/pardibaal/Federation.h
@@ -25,7 +25,7 @@
 #include <vector>
 #include <ostream>
 
-#include "clock_constraint_t.h"
+#include "difference_bound_t.h"
 #include "bound_t.h"
 #include "DBM.h"
 
@@ -78,6 +78,16 @@ namespace pardibaal {
          */
         void add(const Federation& fed);
 
+        /**
+         * Subtract everything that satisfies the constraint i - j </<= bound constraint
+         */
+        void subtract(dim_t i, dim_t j, bound_t bound);
+
+        /**
+         * Subtract everything that satisfies the difference constraint
+         */
+        void subtract(difference_bound_t constraint);
+
         /**
          * Subtract a dbm from this federation.
          * @param dbm to be subtracted.
@@ -122,8 +132,8 @@ namespace pardibaal {
          */
         [[nodiscard]] bool is_satisfying(dim_t x, dim_t y, bound_t g) const;
 
-        [[nodiscard]] bool is_satisfying(const clock_constraint_t& constraint) const;
-        [[nodiscard]] bool is_satisfying(const std::vector<clock_constraint_t>& constraints) const;
+        [[nodiscard]] bool is_satisfying(const difference_bound_t& constraint) const;
+        [[nodiscard]] bool is_satisfying(const std::vector<difference_bound_t>& constraints) const;
 
         /**
          * Relation between this and a dbm.
@@ -229,13 +239,13 @@ namespace pardibaal {
          * Checks if a federation intersect with a federation ie. if the intersection is non-empty
          * @return true if this intersects with dbm
          */
-        [[nodiscard]] bool intersects(const DBM& dbm) const;
+        [[nodiscard]] bool is_intersecting(const DBM& dbm) const;
 
         /**
          * Checks if a federation intersect with a DBM ie. if the intersection is non-empty
          * @return true if this intersects with fed
          */
-        [[nodiscard]] bool intersects(const Federation& fed) const;
+        [[nodiscard]] bool is_intersecting(const Federation& fed) const;
 
         /**
          * Checks if the any of the zones have upper bounds
@@ -251,8 +261,8 @@ namespace pardibaal {
         void interval_delay(val_t lower, val_t upper);
 
         void restrict(dim_t x, dim_t y, bound_t g);
-        void restrict(const clock_constraint_t& constraint);
-        void restrict(const std::vector<clock_constraint_t>& constraints);
+        void restrict(const difference_bound_t& constraint);
+        void restrict(const std::vector<difference_bound_t>& constraints);
         void free(dim_t x);
         void assign(dim_t x, val_t m);
         void copy(dim_t x, dim_t y);

diff --git a/src/pardibaal/bound_t.cpp b/src/pardibaal/bound_t.cpp
@@ -26,7 +26,7 @@
 
 namespace pardibaal {
 
-    bound_t::bound_t(val_t n, strict_t strictness) : _n(n) {_strict = strictness == STRICT ? true : false;}
+    bound_t::bound_t(val_t n, strict_e strictness) : _n(n) {_strict = strictness == STRICT ? true : false;}
 
     bound_t::bound_t(val_t n, bool strict) : _n(n), _strict(strict) {}
 
@@ -110,6 +110,13 @@ namespace pardibaal {
     bool bound_t::operator>=(bound_t rhs) const {return not (*this < rhs);}
     bool bound_t::operator<=(bound_t rhs) const {return not (rhs < *this);}
 
+    bool bound_t::operator==(val_t rhs) const {return *this == bound_t::non_strict(rhs);}
+    bool bound_t::operator!=(val_t rhs) const {return *this != bound_t::non_strict(rhs);}
+    bool bound_t::operator<(val_t rhs) const {return *this < bound_t::non_strict(rhs);}
+    bool bound_t::operator>(val_t rhs) const {return *this > bound_t::non_strict(rhs);}
+    bool bound_t::operator<=(val_t rhs) const {return *this <= bound_t::non_strict(rhs);}
+    bool bound_t::operator>=(val_t rhs) const {return *this >= bound_t::non_strict(rhs);}
+
     bool lt(bound_t lhs, bound_t rhs) {return lhs < rhs;}
     bool le(bound_t lhs, bound_t rhs) {return lhs <= rhs;}
     bool gt(bound_t lhs, bound_t rhs) {return lhs > rhs;}

diff --git a/src/pardibaal/bound_t.h b/src/pardibaal/bound_t.h
@@ -31,7 +31,7 @@ namespace pardibaal {
     using dim_t = uint32_t;
     using val_t = int32_t;
 
-    enum strict_t {STRICT, NON_STRICT};
+    enum strict_e {STRICT, NON_STRICT};
 
     struct bound_t {
     private:
@@ -40,7 +40,7 @@ namespace pardibaal {
              _inf = false;
     public:
         bound_t(){};
-        bound_t(val_t n, strict_t strictness);
+        bound_t(val_t n, strict_e strictness);
         bound_t(val_t n, bool strict);
 
         [[nodiscard]] static bound_t strict(val_t n);
@@ -78,6 +78,13 @@ namespace pardibaal {
         [[nodiscard]] bool operator>=(bound_t rhs) const;
         [[nodiscard]] bool operator<=(bound_t rhs) const;
 
+        [[nodiscard]] bool operator==(val_t rhs) const;
+        [[nodiscard]] bool operator!=(val_t rhs) const;
+        [[nodiscard]] bool operator<(val_t rhs) const;
+        [[nodiscard]] bool operator>(val_t rhs) const;
+        [[nodiscard]] bool operator<=(val_t rhs) const;
+        [[nodiscard]] bool operator>=(val_t rhs) const;
+
         friend std::ostream& operator<<(std::ostream& out, const bound_t& bound);
 
         [[nodiscard]] static bool is_lt(bound_t lhs, bound_t rhs) {return lhs < rhs;}