← Back to branch summary

~verifypn-cpn/verifypn/cfp_point-wise

« back to all changes in this revision

Viewing changes to src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp

  • Committer: tpede16 at aau
  • Date: 2020-12-16 14:40:32 UTC
  • Revision ID: tpede16@student.aau.dk-20201216144032-pmwykobgleltmncg
Add dot color on output arcs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/PetriEngine/Colored/ColoredPetriNetBuilder.cpp
169
169
                if (transition.considered) break;
170
170
                bool transitionActivated = true;
171
171
                //maybe this can be avoided with a better implementation
172
 
                transition.variableMap.clear();
 
172
                transition.variableMaps.clear();
 
173
 
 
174
                //std::cout << "Transtition " << transition.name << std::endl;
173
175
 
174
176
                if(!_arcIntervals.count(transitionId)){
175
177
                    _arcIntervals[transitionId] = setupTransitionVars(transition);
223
225
            arcInterval._intervalTupleVec.clear();
224
226
 
225
227
            if(!arc.expr->getArcIntervals(arcInterval, curCFP, &index, 0)){
226
 
                std::cout << "Failed to get arc intervals" << std::endl;
 
228
                //std::cout << "Failed to get arc intervals" << std::endl;
227
229
                transitionActivated = false;
228
230
                return;
229
231
            } 
230
232
        }
231
 
        if(getVarIntervals(transition.variableMap, transitionId)){
 
233
        if(getVarIntervals(transition.variableMaps, transitionId)){
232
234
            // std::cout << transition.name << " var intervals" << std::endl;
233
235
            // for (auto pair : transition.variableMap){
234
236
            //     std::cout << "Var set:" << std::endl;
238
240
            //     }
239
241
            // }
240
242
            if(transition.guard != nullptr) {
241
 
                transition.guard->restrictVars(transition.variableMap);
 
243
                transition.guard->restrictVars(transition.variableMaps);
242
244
                std::vector<uint32_t> invalidIds;
243
245
 
244
 
                for(uint32_t i = 0; i < transition.variableMap.size(); i++){      
245
 
                    for(auto varPair : transition.variableMap[i]){
 
246
                for(uint32_t i = 0; i < transition.variableMaps.size(); i++){      
 
247
                    for(auto varPair : transition.variableMaps[i]){
246
248
                        if(!varPair.second.hasValidIntervals()){
247
249
                            invalidIds.push_back(i);
248
250
                            break;
250
252
                    }                    
251
253
                }
252
254
                for(auto id = invalidIds.rbegin(); id != invalidIds.rend(); id++){
253
 
                    transition.variableMap.erase(transition.variableMap.begin() + *id);
 
255
                    transition.variableMaps.erase(transition.variableMaps.begin() + *id);
254
256
                }
255
257
 
256
 
                if(transition.variableMap.empty()){
 
258
                if(transition.variableMaps.empty()){
257
259
                    std::cout << "Guard restrictions removed all valid intervals" << std::endl;
258
260
                    transitionActivated = false;
259
261
                    return;
266
268
    }
267
269
 
268
270
 
269
 
    bool ColoredPetriNetBuilder::getVarIntervals(std::vector<std::unordered_map<const Colored::Variable *, Reachability::intervalTuple_t>>& variableMap, uint32_t transitionId){
 
271
    bool ColoredPetriNetBuilder::getVarIntervals(std::vector<std::unordered_map<const Colored::Variable *, Reachability::intervalTuple_t>>& variableMaps, uint32_t transitionId){
270
272
        for(auto& placeArcIntervals : _arcIntervals[transitionId]){
271
273
            
272
274
            for(uint32_t j = 0; j < placeArcIntervals.second._intervalTupleVec.size(); j++){
273
275
                //If we have not found intervals for any place yet, we fill the intervals from this place
274
276
                //Else we restrict the intervals we already found to only keep those that can also be matched in this place
275
 
                if(variableMap.empty()){
 
277
                if(variableMaps.empty()){
276
278
                    for(uint32_t i = 0; i < placeArcIntervals.second._intervalTupleVec[j].size(); i++){
277
279
                        std::unordered_map<const Colored::Variable *, Reachability::intervalTuple_t> localVarMap;
278
280
                        bool validInterval = true;
319
321
                        }
320
322
 
321
323
                        if(validInterval){
322
 
                            variableMap.push_back(localVarMap);
 
324
                            variableMaps.push_back(localVarMap);
323
325
                        }  
324
326
                    }                               
325
327
                } else {
326
 
                    std::vector<std::unordered_map<const Colored::Variable *, Reachability::intervalTuple_t>> newVarMap;
 
328
                    std::vector<std::unordered_map<const Colored::Variable *, Reachability::intervalTuple_t>> newVarMapVec;
327
329
 
328
 
                    for(auto varMap : variableMap){                    
 
330
                    for(auto varMap : variableMaps){                    
329
331
                        for(uint32_t i = 0; i < placeArcIntervals.second._intervalTupleVec[j].size(); i++){
330
332
                            std::unordered_map<const Colored::Variable *, Reachability::intervalTuple_t> localVarMap;
331
333
                            bool allVarsAssigned = true;
391
393
                            }
392
394
 
393
395
                            if(allVarsAssigned){
394
 
                                newVarMap.push_back(localVarMap);
 
396
                                newVarMapVec.push_back(localVarMap);
395
397
                            }       
396
398
                        }                                      
397
399
                    }
398
 
                    variableMap = newVarMap; 
 
400
                    variableMaps = newVarMapVec; 
399
401
                }
400
402
                //If we did not find any intervals for an arc, then the transition cannot be activated
401
 
                if(variableMap.empty()){
 
403
                if(variableMaps.empty()){
402
404
                    return false;
403
405
                }                          
404
406
            }
446
448
    void ColoredPetriNetBuilder::processOutputArcs(Colored::Transition& transition) {
447
449
        bool transitionHasVarOutArcs = false;
448
450
 
 
451
        // std::cout << "Transistion " << transition.name << " activated" << std::endl;
 
452
        // std::cout << "Vars bound to " << std::endl;
 
453
        // for(auto varmap : transition.variableMap){
 
454
        //     std::cout << "Var set:" << std::endl;
 
455
        //     for(auto pair : varmap){
 
456
        //         std::cout << pair.first->name << std::endl;
 
457
        //         pair.second.print();
 
458
        //     }
 
459
        // }
 
460
 
449
461
        for (auto& arc : transition.output_arcs) {
450
462
            Colored::ColorFixpoint& placeFixpoint = _placeColorFixpoints[arc.place];
451
463
 
467
479
            if (!variables.empty()) {
468
480
                transitionHasVarOutArcs = true;
469
481
            }
470
 
            auto intervals = arc.expr->getOutputIntervals(transition.variableMap);
471
 
 
472
 
            intervals.simplify();            
 
482
            auto intervals = arc.expr->getOutputIntervals(transition.variableMaps);
 
483
 
 
484
            intervals.simplify();
 
485
 
 
486
            // std::cout << "Output intervals for arc expr " << arc.expr.get()->toString() << std::endl;
 
487
            // intervals.print();
473
488
 
474
489
            for(auto interval : intervals._intervals){
475
490
                placeFixpoint.constraints.addInterval(interval);    
698
713
            assert(arc.expr != nullptr);
699
714
            arc.expr->getVariables(variables);
700
715
        }
 
716
 
 
717
        //  std::cout << _transition.name << " varmap size " << _transition.variableMaps.size() << std::endl;
 
718
        // for(auto varMap : _transition.variableMaps){
 
719
        //     std::cout << "Var set:" << std::endl;
 
720
        //     for(auto pair : varMap){
 
721
        //         std::cout << pair.first->name << "\t";
 
722
        //         for(auto interval : pair.second._intervals){
 
723
        //             interval.print();
 
724
        //             std::cout << " ";
 
725
        //         }
 
726
        //         std::cout << std::endl;
 
727
        //     }
 
728
        // }
701
729
        
702
730
        for (auto var : variables) {
703
 
            if(_transition.variableMap.empty() || _transition.variableMap[_nextIndex][var]._intervals.empty()){
 
731
            if(_transition.variableMaps.empty() || _transition.variableMaps[_nextIndex][var]._intervals.empty()){
704
732
                _noValidBindings = true;
705
733
                break;
706
734
            }
707
 
            auto color = var->colorType->getColor(_transition.variableMap[_nextIndex][var].getFirst().getLowerIds());
 
735
            auto color = var->colorType->getColor(_transition.variableMaps[_nextIndex][var].getFirst().getLowerIds());
708
736
            _bindings[var] = color;
709
737
        }
710
738
        
731
759
        while (!test) {
732
760
            bool next = true;
733
761
            for (auto& _binding : _bindings) {
734
 
                auto varInterval = _transition.variableMap[_nextIndex][_binding.first];
 
762
                auto varInterval = _transition.variableMaps[_nextIndex][_binding.first];
735
763
                std::vector<uint32_t> colorIds;
736
764
                _binding.second->getTupleId(&colorIds);
737
765
                auto nextIntervalBinding = varInterval.isRangeEnd(colorIds);
755
783
                    break;
756
784
                }
757
785
                for(auto& _binding : _bindings){
758
 
                    _binding.second =  _binding.second->getColorType()->getColor(_transition.variableMap[_nextIndex][_binding.first].getFirst().getLowerIds());
 
786
                    _binding.second =  _binding.second->getColorType()->getColor(_transition.variableMaps[_nextIndex][_binding.first].getFirst().getLowerIds());
759
787
                }
760
788
            }
761
789
                 
771
799
    }
772
800
 
773
801
    bool BindingGenerator::isInitial() const{        
774
 
        return _nextIndex >= _transition.variableMap.size();
 
802
        return _nextIndex >= _transition.variableMaps.size();
775
803
    }
776
804
 
777
805
    BindingGenerator::Iterator BindingGenerator::begin() {