← Back to branch summary

~tapaal-contributor/verifypn/Fix-partition-id-clash-1939939

« back to all changes in this revision

Viewing changes to include/LTL/Algorithm/ModelChecker.h

  • Committer: Jiri Srba
  • Date: 2021-08-09 09:05:47 UTC
  • mfrom: (246.1.5 ltl-fixes)
  • Revision ID: srba.jiri@gmail.com-20210809090547-etvsii2b4zlya5au
merged in lp:~tapaal-ltl/verifypn/ltl-trace-fixes fixing trace generation and replay

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/LTL/Algorithm/ModelChecker.h
115
115
            if (traceLevel == TraceLevel::Full) {
116
116
                os << ">";
117
117
                os << std::endl;
118
 
                for (size_t i = 0; i < net->numberOfPlaces(); ++i) {
 
118
                auto [fpre, lpre] = net->preset(transition);
 
119
                for(; fpre < lpre; ++fpre) {
 
120
                    if (fpre->inhibitor) {
 
121
                        assert(state.marking()[fpre->place] < fpre->tokens);
 
122
                        continue;
 
123
                    }
 
124
                    for (size_t i = 0; i < fpre->tokens; ++i) {
 
125
                        assert(state.marking()[fpre->place] >= fpre->tokens);
 
126
                        os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[fpre->place] << "\"/>\n";
 
127
                    }
 
128
                }
 
129
                /*for (size_t i = 0; i < net->numberOfPlaces(); ++i) {
119
130
                    for (size_t j = 0; j < state.marking()[i]; ++j) {
120
131
                        os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[i] << "\"/>\n";
121
132
                    }
122
 
                }
 
133
                }*/
123
134
                os << indent << "</transition>";
124
135
            }
125
136
            else {