~tapaal-ltl/verifypn/fireable-empty-preset-fix : contents of src/PetriEngine/Colored/EquivalenceClass.cpp at revision 243

~tapaal-ltl/verifypn/fireable-empty-preset-fix : (revision 243)

#include "PetriEngine/Colored/EquivalenceClass.h"

namespace PetriEngine {
    namespace Colored {


        EquivalenceClass::EquivalenceClass(uint32_t id) : _id(id){
        }
        EquivalenceClass::EquivalenceClass(uint32_t id, const ColorType *colorType)
        : _id(id), _colorType(colorType){
        }
        EquivalenceClass::EquivalenceClass(uint32_t id, const ColorType *colorType, interval_vector_t&& colorIntervals)
        : _id(id), _colorType(colorType), _colorIntervals(std::move(colorIntervals)){
        }

        EquivalenceClass EquivalenceClass::intersect(uint32_t id, const EquivalenceClass &other) const{
            EquivalenceClass result = EquivalenceClass(id);

            if(_colorType != other._colorType){
                return result;
            }
            result._colorType = _colorType;

            for(const auto& interval : _colorIntervals){
                for(const auto& otherInterval : other._colorIntervals){
                    auto overlappingInterval = interval.getOverlap(otherInterval);
                    if(overlappingInterval.isSound()){
                        result._colorIntervals.addInterval(overlappingInterval);
                    }
                }
            }
            return result;
        }


        EquivalenceClass EquivalenceClass::subtract(uint32_t id, const EquivalenceClass &other, const std::vector<bool> &diagonalPositions) const{
            EquivalenceClass result = EquivalenceClass(id);
            if(_colorType != other._colorType){
                return result;
            }
            result._colorType = _colorType;
            interval_vector_t resIntervals;
            for(const auto& interval : _colorIntervals){
                interval_vector_t intervalSubRes;
                for(const auto& otherInterval : other._colorIntervals){
                    auto subtractedIntervals = interval.getSubtracted(otherInterval, diagonalPositions);
                    

                    if(subtractedIntervals.empty() || subtractedIntervals[0].size() == 0){
                        intervalSubRes.clear();
                        break;                           
                    }

                    if(intervalSubRes.empty()){
                        intervalSubRes = subtractedIntervals;
                    } else {
                        interval_vector_t newIntervals;
                        for(const auto& newInterval : subtractedIntervals){
                            for(const auto& interval : intervalSubRes){
                                auto intersection = interval.getOverlap(newInterval);
                                if(intersection.isSound()){
                                    newIntervals.addInterval(intersection);
                                }
                            }
                        }
                        intervalSubRes = std::move(newIntervals);                              
                    }
                }
                for(const auto& interval : intervalSubRes){
                    resIntervals.addInterval(interval);
                }                
            }
            result._colorIntervals = resIntervals;                  
            return result;
        }

        bool EquivalenceClass::containsColor(const std::vector<uint32_t> &ids, const std::vector<bool> &diagonalPositions) const {
            if(ids.size() != _colorIntervals.front().size()){
                return false;
            }
            for(const auto &interval : _colorIntervals){
                bool contained = true;
                for(uint32_t i = 0; i < ids.size(); i++){
                    if(!diagonalPositions[i] && !interval[i].contains(ids[i])){
                        contained = false;
                        break;
                    }
                }
                if(contained){
                    return true;
                }
            }
            return false;
        }

        size_t EquivalenceClass::size() const{
            size_t result = 0;
            for(const auto& interval : _colorIntervals){
                size_t intervalSize = 1;
                for(const auto& range : interval._ranges){
                    intervalSize *= range.size();
                }
                result += intervalSize;
            }
            return result;
        }
    }
}

227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	1	#include "PetriEngine/Colored/EquivalenceClass.h"
	2
	3	namespace PetriEngine {
	4	namespace Colored {
	5
233.1.38 by Peter G. Jensen cleaning up types & refactoring	6
	7	EquivalenceClass::EquivalenceClass(uint32_t id) : _id(id){
	8	}
	9	EquivalenceClass::EquivalenceClass(uint32_t id, const ColorType *colorType)
	10	: _id(id), _colorType(colorType){
	11	}
	12	EquivalenceClass::EquivalenceClass(uint32_t id, const ColorType *colorType, interval_vector_t&& colorIntervals)
	13	: _id(id), _colorType(colorType), _colorIntervals(std::move(colorIntervals)){
	14	}
	15
	16	EquivalenceClass EquivalenceClass::intersect(uint32_t id, const EquivalenceClass &other) const{
	17	EquivalenceClass result = EquivalenceClass(id);
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	18
	19	if(_colorType != other._colorType){
	20	return result;
	21	}
	22	result._colorType = _colorType;
	23
233.1.38 by Peter G. Jensen cleaning up types & refactoring	24	for(const auto& interval : _colorIntervals){
233.1.38 by Peter G. Jensen cleaning up types & refactoring	25	for(const auto& otherInterval : other._colorIntervals){
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	26	auto overlappingInterval = interval.getOverlap(otherInterval);
	27	if(overlappingInterval.isSound()){
	28	result._colorIntervals.addInterval(overlappingInterval);
	29	}
	30	}
	31	}
	32	return result;
	33	}
	34
	35
233.1.38 by Peter G. Jensen cleaning up types & refactoring	36	EquivalenceClass EquivalenceClass::subtract(uint32_t id, const EquivalenceClass &other, const std::vector<bool> &diagonalPositions) const{
233.1.38 by Peter G. Jensen cleaning up types & refactoring	37	EquivalenceClass result = EquivalenceClass(id);
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	38	if(_colorType != other._colorType){
	39	return result;
	40	}
	41	result._colorType = _colorType;
233.1.38 by Peter G. Jensen cleaning up types & refactoring	42	interval_vector_t resIntervals;
	43	for(const auto& interval : _colorIntervals){
	44	interval_vector_t intervalSubRes;
	45	for(const auto& otherInterval : other._colorIntervals){
233.1.42 by tpede16 at aau Implement var resrictions for inequality	46	auto subtractedIntervals = interval.getSubtracted(otherInterval, diagonalPositions);
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	47
	48
	49	if(subtractedIntervals.empty() \|\| subtractedIntervals[0].size() == 0){
233.1.38 by Peter G. Jensen cleaning up types & refactoring	50	intervalSubRes.clear();
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	51	break;
	52	}
	53
233.1.38 by Peter G. Jensen cleaning up types & refactoring	54	if(intervalSubRes.empty()){
233.1.38 by Peter G. Jensen cleaning up types & refactoring	55	intervalSubRes = subtractedIntervals;
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	56	} else {
233.1.38 by Peter G. Jensen cleaning up types & refactoring	57	interval_vector_t newIntervals;
233.1.37 by Peter G. Jensen more const-ref, in particular in loops. Removed some pointers also	58	for(const auto& newInterval : subtractedIntervals){
233.1.38 by Peter G. Jensen cleaning up types & refactoring	59	for(const auto& interval : intervalSubRes){
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	60	auto intersection = interval.getOverlap(newInterval);
	61	if(intersection.isSound()){
	62	newIntervals.addInterval(intersection);
	63	}
	64	}
	65	}
233.1.14 by tpede16 at aau Fix comments, split up functions and add typedefs	66	intervalSubRes = std::move(newIntervals);
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	67	}
	68	}
233.1.38 by Peter G. Jensen cleaning up types & refactoring	69	for(const auto& interval : intervalSubRes){
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	70	resIntervals.addInterval(interval);
233.1.14 by tpede16 at aau Fix comments, split up functions and add typedefs	71	}
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	72	}
	73	result._colorIntervals = resIntervals;
	74	return result;
	75	}
	76
233.1.30 by tpede16 at aau Move EquivalenceVec to class	77	bool EquivalenceClass::containsColor(const std::vector<uint32_t> &ids, const std::vector<bool> &diagonalPositions) const {
233.1.15 by Peter G. Jensen less moving, more const	78	if(ids.size() != _colorIntervals.front().size()){
233.1.14 by tpede16 at aau Fix comments, split up functions and add typedefs	79	return false;
	80	}
233.1.38 by Peter G. Jensen cleaning up types & refactoring	81	for(const auto &interval : _colorIntervals){
233.1.14 by tpede16 at aau Fix comments, split up functions and add typedefs	82	bool contained = true;
	83	for(uint32_t i = 0; i < ids.size(); i++){
233.1.26 by tpede16 at aau Fix creation of equivalence classes	84	if(!diagonalPositions[i] && !interval[i].contains(ids[i])){
233.1.14 by tpede16 at aau Fix comments, split up functions and add typedefs	85	contained = false;
	86	break;
	87	}
	88	}
	89	if(contained){
	90	return true;
	91	}
	92	}
	93	return false;
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	94	}
	95
233.1.30 by tpede16 at aau Move EquivalenceVec to class	96	size_t EquivalenceClass::size() const{
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	97	size_t result = 0;
233.1.38 by Peter G. Jensen cleaning up types & refactoring	98	for(const auto& interval : _colorIntervals){
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	99	size_t intervalSize = 1;
233.1.37 by Peter G. Jensen more const-ref, in particular in loops. Removed some pointers also	100	for(const auto& range : interval._ranges){
227.6.10 by tpede16 at aau Fix token distribution, .all arcs and place unfolding	101	intervalSize *= range.size();
	102	}
	103	result += intervalSize;
	104	}
	105	return result;
	106	}
	107	}
	108	}