« back to all changes in this revision
Viewing changes to PetriEngine/Reducer.cpp
- browse files at revision 200
- compare with another revision
- download diff
- download tarball
- view history from revision 200
- Committer: Jiri Srba
- Date: 2018-04-18 10:58:36 UTC
- mfrom: (197.3.78 cpn_ctlss)
- Revision ID: srba.jiri@gmail.com-20180418105836-a5rha272u0om4u77
merged in branch lp:~verifypn-cpn/verifypn/cpn_ctlss/
CPN unfolding
CPN linear overapproximation
Export of reduced queries and model
parallel query simplification
TAR for P/T nets
Improved structural reduction rules
CPN unfolding
CPN linear overapproximation
Export of reduced queries and model
parallel query simplification
TAR for P/T nets
Improved structural reduction rules
- files added:
- CMakeLists.txt
- PetriEngine/Colored
- PetriEngine/TAR
- Scripts/Comparison
- files removed:
- CTL/SearchStrategy/DFSSearch.cpp
- files modified:
- .bzrignore
added
removed
PetriEngine/Reducer.cpp
11
11
#include <PetriParse/PNMLParser.h>
12
12
#include <queue>
13
13
#include <set>
14
#include <algorithm>
14
15
15
16
namespace PetriEngine {
16
17
17
18
Reducer::Reducer(PetriNetBuilder* p)
18
: _removedTransitions(0), _removedPlaces(0), _ruleA(0), _ruleB(0), _ruleC(0), _ruleD(0), _ruleE(0), _ruleF(0), parent(p) {
19
: parent(p) {
19
20
}
20
21
21
22
Reducer::~Reducer() {
94
95
return ait;
95
96
}
96
97
else
97
{
98
{
98
99
return trans.post.end();
99
}
100
100
}
101
}
101
102
102
103
ArcIter Reducer::getInArc(uint32_t place, Transition& trans)
103
104
{
110
111
}
111
112
else
112
113
{
113
return trans.pre.end();
114
return trans.pre.end();
114
115
}
115
116
}
116
117
483
484
484
485
for(size_t swp = 0; swp < 2; ++swp)
485
486
{
487
if(hasTimedout()) return false;
486
488
if( parent->_places[pinner].skip ||
487
489
parent->_places[pouter].skip) break;
488
490
503
505
Place& place2 = parent->_places[p2];
504
506
505
507
// C2, C3. Consumer and producer-sets must match
506
if(place1.consumers.size() != place2.consumers.size() ||
507
place1.producers.size() != place2.producers.size())
508
if(place1.consumers.size() < place2.consumers.size() ||
509
place1.producers.size() > place2.producers.size())
508
510
break;
509
511
510
uint mult = std::numeric_limits<uint>::max();
512
long double mult = 1;
511
513
512
514
// C8. Consumers must match with weights
513
515
int ok = 0;
514
for(int i = place1.consumers.size() - 1; i >= 0; --i)
516
size_t j = 0;
517
for(size_t i = 0; i < place2.consumers.size(); ++i)
515
518
{
516
if(place1.consumers[i] != place2.consumers[i])
519
while(j < place1.consumers.size() && place1.consumers[j] < place2.consumers[i] ) ++j;
520
if(place1.consumers.size() <= j || place1.consumers[j] != place2.consumers[i])
517
521
{
518
522
ok = 2;
519
523
break;
520
524
}
521
525
522
Transition& trans = getTransition(place1.consumers[i]);
526
Transition& trans = getTransition(place1.consumers[j]);
523
527
auto a1 = getInArc(p1, trans);
524
528
auto a2 = getInArc(p2, trans);
525
if(a2 == trans.pre.end())
526
{
527
ok = 2;
528
break;
529
}
530
529
assert(a1 != trans.pre.end());
531
532
if(mult == std::numeric_limits<uint>::max())
533
{
534
if(a2->weight < a1->weight || (a2->weight % a1->weight) != 0)
535
{
536
ok = 1;
537
break;
538
}
539
mult = a2->weight / a1->weight;
540
}
541
else if(a1->weight*mult != a2->weight)
542
{
543
ok = 2;
544
break;
545
}
530
assert(a2 != trans.pre.end());
531
mult = std::max(mult, ((long double)a2->weight) / ((long double)a1->weight));
546
532
}
547
533
548
534
if(ok == 2) break;
549
else if(ok == 1) continue;
550
535
536
// C6. We do not care about excess markings in p2.
537
if(mult != std::numeric_limits<long double>::max() &&
538
(((long double)parent->initialMarking[p1]) * mult) > ((long double)parent->initialMarking[p2]))
539
{
540
continue;
541
}
542
543
551
544
// C7. Producers must match with weights
552
for(int i = place1.producers.size() - 1; i >= 0; --i)
545
j = 0;
546
for(size_t i = 0; i < place1.producers.size(); ++i)
553
547
{
554
if(place1.producers[i] != place2.producers[i])
548
while(place2.producers[j] < place1.producers[i] && j < place2.producers.size()) ++j;
549
if(place1.producers[i] != place2.producers[j])
555
550
{
556
551
ok = 2;
557
552
break;
560
555
Transition& trans = getTransition(place1.producers[i]);
561
556
auto a1 = getOutArc(trans, p1);
562
557
auto a2 = getOutArc(trans, p2);
563
if( a2 == trans.post.end())
564
{
565
ok = 2;
566
break;
567
}
568
558
assert(a1 != trans.post.end());
569
if(mult == std::numeric_limits<uint>::max())
570
{
571
if(a2->weight < a1->weight || (a2->weight % a1->weight) != 0)
572
{
573
ok = 1;
574
break;
575
}
576
mult = a2->weight / a1->weight;
577
}
578
else if(a1->weight*mult != a2->weight)
579
{
580
ok = 2;
559
assert(a2 != trans.post.end());
560
561
if(((long double)a1->weight)*mult > ((long double)a2->weight))
562
{
563
ok = 1;
581
564
break;
582
565
}
583
566
}
585
568
if(ok == 2) break;
586
569
else if(ok == 1) continue;
587
570
588
// C6. We do not care about excess markings in p2.
589
if(mult != std::numeric_limits<uint>::max() &&
590
(parent->initialMarking[p1] * mult) > parent->initialMarking[p2])
591
continue;
592
593
571
parent->initialMarking[p2] = 0;
594
572
595
573
if(reconstructTrace)
628
606
if (tout.inhib) continue;
629
607
630
608
for (uint32_t tinner = touter + 1; tinner < ntrans; ++tinner) {
631
632
609
Transition& tin = getTransition(tinner);
633
610
if (tin.skip || tout.skip) continue;
634
611
636
613
if (tin.inhib) continue;
637
614
638
615
for (size_t swp = 0; swp < 2; ++swp) {
616
if(hasTimedout()) return false;
639
617
640
618
if (tin.skip || tout.skip) break;
641
619
726
704
Place& place = parent->_places[p];
727
705
if(place.skip) continue;
728
706
if(place.inhib) continue;
729
if(placeInQuery[p] > 0) continue;
730
707
if(place.producers.size() > place.consumers.size()) continue;
731
708
732
709
std::set<uint32_t> notenabled;
733
bool ok = true;
710
bool ok = true;
734
711
for(uint cons : place.consumers)
735
712
{
736
713
Transition& t = getTransition(cons);
737
if(getInArc(p, t)->weight <= parent->initialMarking[p])
714
auto in = getInArc(p, t);
715
if(in->weight <= parent->initialMarking[p])
738
716
{
739
ok = false;
740
break;
717
auto out = getOutArc(t, p);
718
if(out == t.post.end() || out->place != p || out->weight >= in->weight)
719
{
720
ok = false;
721
break;
722
}
741
723
}
742
724
else
743
725
{
745
727
}
746
728
}
747
729
748
if(!ok) continue;
730
if(!ok || notenabled.size() == 0) continue;
749
731
750
732
for(uint prod : place.producers)
751
733
{
772
754
773
755
parent->initialMarking[p] = 0;
774
756
775
bool skipplace = notenabled.size() == place.consumers.size();
757
bool skipplace = (notenabled.size() == place.consumers.size()) && (placeInQuery[p] == 0);
776
758
for(uint cons : notenabled)
777
759
skipTransition(cons);
778
760
784
766
return continueReductions;
785
767
}
786
768
769
bool Reducer::ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers) {
770
bool reduced = false;
771
if(remove_loops)
772
{
773
std::vector<uint32_t> wtrans;
774
std::vector<bool> tseen(parent->numberOfTransitions(), false);
775
776
for(uint32_t p = 0; p < parent->numberOfPlaces(); ++p)
777
{
778
if(hasTimedout()) return false;
779
if(placeInQuery[p] > 0)
780
{
781
const Place& place = parent->_places[p];
782
for(auto t : place.consumers)
783
{
784
if(!tseen[t])
785
{
786
wtrans.push_back(t);
787
tseen[t] = true;
788
}
789
}
790
for(auto t : place.producers)
791
{
792
if(!tseen[t])
793
{
794
wtrans.push_back(t);
795
tseen[t] = true;
796
}
797
}
798
}
799
}
800
801
std::vector<bool> pseen(parent->numberOfPlaces(), false);
802
while(!wtrans.empty())
803
{
804
if(hasTimedout()) return false;
805
auto t = wtrans.back();
806
wtrans.pop_back();
807
const Transition& trans = parent->_transitions[t];
808
for(const Arc& arc : trans.pre)
809
{
810
const Place& place = parent->_places[arc.place];
811
if(arc.inhib)
812
{
813
for(auto pt : place.consumers)
814
{
815
if(!tseen[pt])
816
{
817
Transition& trans = parent->_transitions[pt];
818
auto it = trans.post.begin();
819
for(; it != trans.post.end(); ++it)
820
if(it->place >= arc.place) break;
821
if(it != trans.pre.end() && it->place == arc.place)
822
{
823
auto it2 = trans.pre.begin();
824
for(; it2 != trans.pre.end(); ++it2)
825
if(it2->place >= arc.place || it2->inhib) break;
826
if(it->weight <= it2->weight) continue;
827
}
828
tseen[pt] = true;
829
wtrans.push_back(pt);
830
}
831
}
832
}
833
else
834
{
835
for(auto pt : place.producers)
836
{
837
if(!tseen[pt])
838
{
839
Transition& trans = parent->_transitions[pt];
840
auto it = trans.pre.begin();
841
for(; it != trans.pre.end(); ++it)
842
if(it->place >= arc.place) break;
843
844
if(it != trans.pre.end() && it->place == arc.place && !it->inhib)
845
{
846
auto it2 = trans.post.begin();
847
for(; it2 != trans.post.end(); ++it2)
848
if(it2->place >= arc.place) break;
849
if(it->weight >= it2->weight) continue;
850
}
851
852
tseen[pt] = true;
853
wtrans.push_back(pt);
854
}
855
}
856
857
for(auto pt : place.consumers)
858
{
859
if(!tseen[pt] && (!remove_consumers || placeInQuery[arc.place] > 0))
860
{
861
tseen[pt] = true;
862
wtrans.push_back(pt);
863
}
864
}
865
}
866
pseen[arc.place] = true;
867
}
868
}
869
870
for(size_t t = 0; t < parent->numberOfTransitions(); ++t)
871
{
872
if(!tseen[t] && !parent->_transitions[t].skip)
873
{
874
skipTransition(t);
875
reduced = true;
876
}
877
}
878
879
for(size_t p = 0; p < parent->numberOfPlaces(); ++p)
880
{
881
if(!pseen[p] && !parent->_places[p].skip && placeInQuery[p] == 0)
882
{
883
assert(placeInQuery[p] == 0);
884
skipPlace(p);
885
reduced = true;
886
}
887
}
888
889
if(reduced)
890
++_ruleI;
891
}
892
else
893
{
894
const size_t numberofplaces = parent->numberOfPlaces();
895
for(uint32_t p = 0; p < numberofplaces; ++p)
896
{
897
if(hasTimedout()) return false;
898
Place& place = parent->_places[p];
899
if(place.skip) continue;
900
if(place.inhib) continue;
901
if(placeInQuery[p] > 0) continue;
902
if(place.consumers.size() > 0) continue;
903
904
++_ruleI;
905
reduced = true;
906
907
std::vector<uint32_t> torem;
908
for(auto& t : place.producers)
909
{
910
auto& trans = parent->_transitions[t];
911
if(trans.post.size() != 1) // place will be removed later
912
continue;
913
bool ok = true;
914
for(auto& a : trans.pre)
915
{
916
if(placeInQuery[a.place] > 0)
917
{
918
ok = false;
919
}
920
}
921
if(ok) torem.push_back(t);
922
}
923
skipPlace(p);
924
for(auto t : torem)
925
skipTransition(t);
926
assert(consistent());
927
}
928
}
929
930
return reduced;
931
}
932
787
933
bool Reducer::ReducebyRuleF(uint32_t* placeInQuery) {
788
934
bool continueReductions = false;
789
935
const size_t numberofplaces = parent->numberOfPlaces();
793
939
Place& place = parent->_places[p];
794
940
if(place.skip) continue;
795
941
if(place.inhib) continue;
796
if(placeInQuery[p] > 0) continue;
797
if(place.consumers.size() > 0) continue;
942
if(place.producers.size() < place.consumers.size()) continue;
943
if(placeInQuery[p] != 0) continue;
944
945
bool ok = true;
946
for(uint cons : place.consumers)
947
{
948
Transition& t = getTransition(cons);
949
auto w = getInArc(p, t)->weight;
950
if(w > parent->initialMarking[p])
951
{
952
ok = false;
953
break;
954
}
955
else
956
{
957
auto it = getOutArc(t, p);
958
if(it == t.post.end() ||
959
it->place != p ||
960
it->weight < w)
961
{
962
ok = false;
963
break;
964
}
965
}
966
}
967
968
if(!ok) continue;
798
969
799
970
++_ruleF;
800
continueReductions = true;
801
skipPlace(p);
802
std::vector<uint32_t> torem;
803
for(auto& t : place.producers)
804
{
805
auto& trans = parent->_transitions[t];
806
if(trans.post.size() != 0)
807
continue;
808
bool ok = true;
809
for(auto& a : trans.pre)
810
{
811
if(placeInQuery[a.place] > 0)
812
{
813
ok = false;
814
}
815
}
816
if(ok) torem.push_back(t);
817
}
818
819
for(auto t : torem)
820
skipTransition(t);
821
assert(consistent());
822
}
823
return continueReductions;
824
}
825
826
void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout) {
971
972
if((numberofplaces - _removedPlaces) > 1)
973
{
974
skipPlace(p);
975
continueReductions = true;
976
}
977
978
}
979
assert(consistent());
980
return continueReductions;
981
}
982
983
984
bool Reducer::ReducebyRuleG(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers) {
985
if(!remove_loops) return false;
986
bool continueReductions = false;
987
for(uint32_t t = 0; t < parent->numberOfTransitions(); ++t)
988
{
989
if(hasTimedout()) return false;
990
Transition& trans = parent->_transitions[t];
991
if(trans.skip) continue;
992
if(trans.inhib) continue;
993
if(trans.pre.size() < trans.post.size()) continue;
994
if(!remove_loops && trans.pre.size() == 0) continue;
995
996
auto postit = trans.post.begin();
997
auto preit = trans.pre.begin();
998
999
bool ok = true;
1000
while(true)
1001
{
1002
if(preit == trans.pre.end() && postit == trans.post.end())
1003
break;
1004
if(preit == trans.pre.end())
1005
{
1006
ok = false;
1007
break;
1008
}
1009
if(preit->inhib)
1010
{
1011
ok = false;
1012
break;
1013
}
1014
if(postit != trans.post.end() && preit->place == postit->place)
1015
{
1016
if(!remove_consumers && preit->weight != postit->weight)
1017
{
1018
ok = false;
1019
break;
1020
}
1021
if((placeInQuery[preit->place] > 0 && preit->weight != postit->weight) ||
1022
(placeInQuery[preit->place] == 0 && preit->weight < postit->weight))
1023
{
1024
ok = false;
1025
break;
1026
}
1027
++preit;
1028
++postit;
1029
}
1030
else if(postit == trans.post.end() || preit->place < postit->place)
1031
{
1032
if(placeInQuery[preit->place] > 0 || !remove_consumers)
1033
{
1034
ok = false;
1035
break;
1036
}
1037
++preit;
1038
}
1039
else
1040
{
1041
// could not match a post with a pre
1042
ok = false;
1043
break;
1044
}
1045
}
1046
1047
if(!ok) continue;
1048
++_ruleG;
1049
skipTransition(t);
1050
}
1051
assert(consistent());
1052
return continueReductions;
1053
}
1054
1055
bool Reducer::ReducebyRuleH(uint32_t* placeInQuery)
1056
{
1057
bool continueReductions = false;
1058
for(uint32_t t1 = 0; t1 < parent->numberOfTransitions(); ++t1)
1059
{
1060
auto& trans1 = parent->_transitions[t1];
1061
if(trans1.skip) continue;
1062
if(trans1.inhib) continue;
1063
if(trans1.pre.size() != 1) continue;
1064
if(trans1.post.size() != 1) continue;
1065
auto p1 = trans1.pre[0].place;
1066
auto p2 = trans1.post[0].place;
1067
if(trans1.pre[0].weight != 1) continue;
1068
if(trans1.post[0].weight != 1) continue;
1069
if(p1 == p2) continue;
1070
if(placeInQuery[p1] > 0) continue;
1071
if(placeInQuery[p2] > 0) continue;
1072
if(parent->_places[p1].inhib) continue;
1073
if(parent->_places[p2].inhib) continue;
1074
1075
for(uint32_t t2 = t1 + 1; t2 < parent->numberOfTransitions(); ++t2)
1076
{
1077
auto& trans2 = parent->_transitions[t2];
1078
if(trans2.skip) continue;
1079
if(trans2.inhib) continue;
1080
if(trans2.pre.size() != 1) continue;
1081
if(trans2.post.size() != 1) continue;
1082
if(trans2.pre[0].weight != 1) continue;
1083
if(trans2.post[0].weight != 1) continue;
1084
if(trans2.pre[0].place != p2) continue;
1085
if(trans2.post[0].place != p1) continue;
1086
1087
++_ruleH;
1088
skipTransition(t2);
1089
1090
auto& place1 = parent->_places[p1];
1091
auto& place2 = parent->_places[p2];
1092
1093
{
1094
1095
for(auto p2it : place2.consumers)
1096
{
1097
auto& t = parent->_transitions[p2it];
1098
auto arc = getInArc(p2, t);
1099
assert(arc != t.pre.end());
1100
assert(arc->place == p2);
1101
auto a = *arc;
1102
a.place = p1;
1103
auto dest = std::lower_bound(t.pre.begin(), t.pre.end(), a);
1104
if(dest == t.pre.end() || dest->place != p1)
1105
{
1106
t.pre.insert(dest, a);
1107
auto lb = std::lower_bound(place1.consumers.begin(), place1.consumers.end(), p2it);
1108
place1.consumers.insert(lb, p2it);
1109
}
1110
else
1111
{
1112
dest->weight += a.weight;
1113
}
1114
consistent();
1115
}
1116
}
1117
1118
{
1119
auto p2it = place2.producers.begin();
1120
1121
for(;p2it != place2.producers.end(); ++p2it)
1122
{
1123
auto& t = parent->_transitions[*p2it];
1124
Arc a = *getOutArc(t, p2);
1125
a.place = p1;
1126
auto dest = std::lower_bound(t.post.begin(), t.post.end(), a);
1127
if(dest == t.post.end() || dest->place != p1)
1128
{
1129
t.post.insert(dest, a);
1130
auto lb = std::lower_bound(place1.producers.begin(), place1.producers.end(), *p2it);
1131
place1.producers.insert(lb, *p2it);
1132
}
1133
else
1134
{
1135
dest->weight += a.weight;
1136
}
1137
consistent();
1138
}
1139
}
1140
1141
parent->initialMarking[p1] += parent->initialMarking[p2];
1142
1143
skipPlace(p2);
1144
continueReductions = true;
1145
}
1146
}
1147
return continueReductions;
1148
}
1149
1150
void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe) {
827
1151
this->_timeout = timeout;
828
1152
_timer = std::chrono::high_resolution_clock::now();
829
1153
assert(consistent());
832
1156
bool changed = false;
833
1157
do
834
1158
{
1159
if(remove_loops && !next_safe)
1160
ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers);
835
1161
do{
836
1162
changed = false;
837
changed |= ReducebyRuleA(context.getQueryPlaceCount());
838
changed |= ReducebyRuleB(context.getQueryPlaceCount());
1163
if(!next_safe) {
1164
changed |= ReducebyRuleB(context.getQueryPlaceCount());
1165
changed |= ReducebyRuleA(context.getQueryPlaceCount());
1166
}
839
1167
changed |= ReducebyRuleE(context.getQueryPlaceCount());
840
changed |= ReducebyRuleF(context.getQueryPlaceCount());
1168
if(!next_safe)
1169
{
1170
changed |= ReducebyRuleF(context.getQueryPlaceCount());
1171
changed |= ReducebyRuleG(context.getQueryPlaceCount(), remove_loops, remove_consumers);
1172
if(!remove_loops)
1173
changed |= ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers);
1174
}
841
1175
} while(changed && !hasTimedout());
842
1176
// RuleC and RuleD are expensive, so wait with those till nothing else changes
843
changed |= ReducebyRuleD(context.getQueryPlaceCount());
844
1177
changed |= ReducebyRuleC(context.getQueryPlaceCount());
1178
if(!next_safe)
1179
{
1180
changed |= ReducebyRuleD(context.getQueryPlaceCount());
1181
1182
if(!changed)
1183
// Only try RuleH last. It can reduce applicability of other rules.
1184
changed |= ReducebyRuleH(context.getQueryPlaceCount());
1185
}
845
1186
} while(!hasTimedout() && changed);
846
1187
847
} else if (enablereduction == 2) { // for k-boundedness checking only rules A and D are applicable
848
while ( (
849
ReducebyRuleA(context.getQueryPlaceCount()) ||
850
ReducebyRuleD(context.getQueryPlaceCount())
851
) && !hasTimedout()) {
1188
} else if (enablereduction == 2) { // for k-boundedness checking only rules A, D and H are applicable
1189
bool changed = true;
1190
while (changed && !hasTimedout()) {
1191
changed = false;
1192
if(!next_safe)
1193
{
1194
changed |= ReducebyRuleA(context.getQueryPlaceCount());
1195
changed |= ReducebyRuleD(context.getQueryPlaceCount());
1196
changed |= ReducebyRuleH(context.getQueryPlaceCount());
1197
}
852
1198
}
853
1199
}
854
1200
}
Loggerhead is a web-based interface for Breezy
Version: 2.0.1