Merge lp:~verifypn-cpn/verifypn/color-fixpoint into lp:~tapaal-ltl/verifypn/random-fix

[Peter Gjøl Jensen]

Fixing the forward approximation (and unfolding)

[lp:~verifypn-cpn/verifypn/color-fixpoint]

267. By Thomas Pedersen <email address hidden> on 2021-04-14

Merge with random-fix branch

[Peter Gjøl Jensen (peter-gjoel)]

passes tests.

review: Approve

=== modified file 'include/PetriEngine/Colored/Intervals.h'
--- include/PetriEngine/Colored/Intervals.h	2021-03-24 10:39:01 +0000
+++ include/PetriEngine/Colored/Intervals.h	2021-04-14 11:52:25 +0000
@@ -545,8 +545,8 @@
                     }
                     
                     _intervals.erase(_intervals.begin() + closestInterval.intervalId2);
-                    
                 }
+                simplify();
             }
 
             closestIntervals getClosestIntervals(){
@@ -560,7 +560,14 @@
                             for(uint32_t k = 0; k < interval->size(); k++) {
                                 int32_t val1 = otherInterval->operator[](k)._lower - interval->operator[](k)._upper;
                                 int32_t val2 = interval->operator[](k)._lower - otherInterval->operator[](k)._upper;
+                                // int32_t lowerDist = interval->operator[](k)._lower > otherInterval->operator[](k)._lower? 
+                                //     interval->operator[](k)._lower - otherInterval->operator[](k)._lower : 
+                                //     otherInterval->operator[](k)._lower - interval->operator[](k)._lower;
+                                // int32_t upperDist = interval->operator[](k)._upper > otherInterval->operator[](k)._upper? 
+                                //     interval->operator[](k)._upper - otherInterval->operator[](k)._upper : 
+                                //     otherInterval->operator[](k)._upper - interval->operator[](k)._upper;
                                 dist += std::max(0, std::max(val1, val2));
+                                //dist += std::max(upperDist + lowerDist, upperDist + lowerDist + std::max(val1, val2));
                                 if(dist >= currentBest.distance){
                                     break;
                                 }