Merge lp:~verifypn-cpn/verifypn/lp-bounds into lp:verifypn

Proposed by Jiri Srba on 2019-02-07
Status: Needs review
Proposed branch: lp:~verifypn-cpn/verifypn/lp-bounds
Merge into: lp:verifypn
Diff against target: 561 lines (+237/-104)
11 files modified
PetriEngine/PQL/Expressions.cpp (+40/-85)
PetriEngine/PQL/Expressions.h (+17/-6)
PetriEngine/Reachability/ReachabilityResult.h (+1/-1)
PetriEngine/Reachability/ReachabilitySearch.cpp (+1/-1)
PetriEngine/Reachability/ReachabilitySearch.h (+2/-0)
PetriEngine/Reachability/ResultPrinter.cpp (+10/-2)
PetriEngine/Simplification/LinearProgram.cpp (+156/-3)
PetriEngine/Simplification/LinearProgram.h (+1/-1)
PetriParse/QueryBinaryParser.cpp (+7/-3)
VerifyPN.cpp (+1/-1)
makefile.linux64 (+1/-1)
To merge this branch: bzr merge lp:~verifypn-cpn/verifypn/lp-bounds
Reviewer Review Type Date Requested Status
Jiri Srba Needs Fixing on 2019-02-07
Review via email: mp+362850@code.launchpad.net

Commit message

This branch adds improvements and fixes to LP solver and adds this to UpperBound computation.

To post a comment you must log in.
Jiri Srba (srba) wrote :

Tested on MCC18 models and queries and works fine. Significant improvements in the number of answers in UpperBounds.

Jiri Srba (srba) :
review: Approve
Jiri Srba (srba) wrote :

Does not compile on mac.

review: Needs Fixing
lp:~verifypn-cpn/verifypn/lp-bounds updated on 2019-02-11
231. By Peter Gjøl Jensen on 2019-02-11

fix for issue with reload of upperbounds

Unmerged revisions

231. By Peter Gjøl Jensen on 2019-02-11

fix for issue with reload of upperbounds

230. By Peter Gjøl Jensen on 2019-02-06

fixed objective function

229. By Peter Gjøl Jensen on 2019-02-05

fixed flags

228. By Peter Gjøl Jensen on 2019-02-05

overwriting default

227. By Peter Gjøl Jensen on 2019-02-04

added check on precision

226. By Peter Gjøl Jensen on 2019-01-27

added support for cpn overapprox for upperbounds

225. By Peter Gjøl Jensen on 2019-01-27

overwriting value of max, used in constructor

224. By Peter Gjøl Jensen on 2019-01-25

fixed missing LP-cleanup and missing handling of non-optimal values / infinite optima

223. By Peter Gjøl Jensen on 2019-01-25

only optimal value is good enough

222. By Peter Gjøl Jensen on 2019-01-13

missing zero check

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'PetriEngine/PQL/Expressions.cpp'
2--- PetriEngine/PQL/Expressions.cpp 2018-08-25 19:48:34 +0000
3+++ PetriEngine/PQL/Expressions.cpp 2019-02-11 21:18:34 +0000
4@@ -835,14 +835,21 @@
5 return RTRUE;
6 }
7
8+ size_t UnfoldedUpperBoundsCondition::value(const MarkVal* marking)
9+ {
10+ size_t tmp = 0;
11+ for(auto& p : _places)
12+ {
13+ auto val = marking[p._place];
14+ p._maxed_out = (p._max <= val);
15+ tmp += val;
16+ }
17+ return tmp;
18+ }
19+
20 Condition::Result UnfoldedUpperBoundsCondition::evaluate(const EvaluationContext& context) {
21- size_t tmp = 0;
22- for(auto& p : _places)
23- {
24- tmp += context.marking()[p._place];
25- }
26- _bound = std::max(tmp, _bound);
27- return _bound < _max ? RUNKNOWN : RTRUE;
28+ setUpperBound(value(context.marking()));
29+ return _max <= _bound ? RTRUE : RUNKNOWN;
30 }
31
32 /******************** Evaluation - save result ********************/
33@@ -1660,9 +1667,13 @@
34 out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
35 uint32_t size = _places.size();
36 out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
37- out.write(reinterpret_cast<const char*>(&_max), sizeof(size_t));
38+ out.write(reinterpret_cast<const char*>(&_max), sizeof(double));
39+ out.write(reinterpret_cast<const char*>(&_offset), sizeof(double));
40 for(auto& b : _places)
41+ {
42 out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));
43+ out.write(reinterpret_cast<const char*>(&b._max), sizeof(double));
44+ }
45 }
46
47 void NotCondition::toBinary(std::ostream& out) const
48@@ -2795,82 +2806,25 @@
49 Retval UnfoldedUpperBoundsCondition::simplify(SimplificationContext& context) const
50 {
51 std::vector<place_t> next;
52+ std::vector<uint32_t> places;
53 for(auto& p : _places)
54- {
55- auto m2 = memberForPlace(p._place, context);
56- Member m1(1);
57- // test for trivial comparison
58- Trivial eval = m1 >= m2;
59- if(eval != Trivial::Indeterminate) {
60- if(eval == Trivial::False)
61- {
62- continue;
63- }
64- else
65- {
66- next.push_back(p);
67- }
68- } else { // if no trivial case
69- int constant = m2.constant() - m1.constant();
70- m1 -= m2;
71- auto nlp = SingleProgram(context.cache(), std::move(m1), constant, Simplification::OP_LE);
72- if(nlp.satisfiable(context))
73- {
74- next.push_back(p);
75- }
76- }
77- }
78-
79- size_t tmin = 1;
80- size_t tmax = std::numeric_limits<int16_t>::max();
81- if(next.size() > 0)
82- {
83- // lets try to find an upper bound for the places so we can
84- // terminate early if lucky.
85- auto m = memberForPlace(_places[0]._place, context);
86- for(size_t i = 1; i < _places.size(); ++i)
87- {
88- m += memberForPlace(_places[i]._place, context);
89- }
90- while(!context.timeout() && tmin != _max)
91- {
92- if(tmin > std::numeric_limits<uint8_t>::max() && tmax == std::numeric_limits<int16_t>::max())
93- {
94- tmax = std::numeric_limits<size_t>::max();
95- break;
96- }
97- auto mid = (tmax / 2) + (tmin / 2);
98- Member c(mid);
99- Trivial eval = c >= m;
100- if(eval != Trivial::Indeterminate) {
101- if(eval == Trivial::False)
102- {
103- tmax = mid;
104- }
105- else
106- {
107- tmin = mid;
108- }
109- } else { // if no trivial case
110- int constant = m.constant() - c.constant();
111- c -= m;
112- auto nlp = SingleProgram(context.cache(), std::move(c), constant, Simplification::OP_GE);
113- if(!nlp.satisfiable(context))
114- {
115- tmax = mid;
116- }
117- else
118- {
119- tmin = mid;
120- }
121- }
122- }
123- }
124- else
125- {
126- tmax = 0;
127- }
128- return Retval(std::make_shared<UnfoldedUpperBoundsCondition>(next, tmax));
129+ places.push_back(p._place);
130+ const auto nplaces = _places.size();
131+ const auto bounds = LinearProgram::bounds(context, context.getLpTimeout(), places);
132+ double offset = _offset;
133+ for(size_t i = 0; i < nplaces; ++i)
134+ {
135+ if(bounds[i].first != 0 && !bounds[i].second)
136+ next.emplace_back(_places[i], bounds[i].first);
137+ if(bounds[i].second)
138+ offset += bounds[i].first;
139+ }
140+ if(bounds[nplaces].second)
141+ {
142+ next.clear();
143+ return Retval(std::make_shared<UnfoldedUpperBoundsCondition>(next, 0, bounds[nplaces].first + _offset));
144+ }
145+ return Retval(std::make_shared<UnfoldedUpperBoundsCondition>(next, bounds[nplaces].first-offset, offset));
146 }
147
148 /******************** Check if query is a reachability query ********************/
149@@ -3536,7 +3490,7 @@
150 std::cerr << "UPPER BOUNDS CANNOT BE NEGATED!" << std::endl;
151 exit(ErrorCode);
152 }
153- return std::make_shared<UnfoldedUpperBoundsCondition>(_places, _max);
154+ return std::make_shared<UnfoldedUpperBoundsCondition>(_places, _max, _offset);
155 }
156
157
158@@ -3853,7 +3807,8 @@
159
160 void UnfoldedUpperBoundsCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
161 for(auto& p : _places)
162- generator.presetOf(p._place);
163+ if(!p._maxed_out)
164+ generator.presetOf(p._place);
165 }
166
167
168
169=== modified file 'PetriEngine/PQL/Expressions.h'
170--- PetriEngine/PQL/Expressions.h 2018-08-25 19:48:34 +0000
171+++ PetriEngine/PQL/Expressions.h 2019-02-11 21:18:34 +0000
172@@ -1195,10 +1195,18 @@
173 struct place_t {
174 std::string _name;
175 uint32_t _place = 0;
176+ double _max = std::numeric_limits<double>::infinity();
177+ bool _maxed_out = false;
178 place_t(const std::string& name)
179 {
180 _name = name;
181 }
182+ place_t(const place_t& other, double max)
183+ {
184+ _name = other._name;
185+ _place = other._place;
186+ _max = max;
187+ }
188 bool operator<(const place_t& other) const{
189 return _place < other._place;
190 }
191@@ -1208,13 +1216,14 @@
192 {
193 for(auto& s : places) _places.push_back(s);
194 }
195- UnfoldedUpperBoundsCondition(const std::vector<place_t>& places, size_t max)
196- : _places(places), _max(max) {
197+ UnfoldedUpperBoundsCondition(const std::vector<place_t>& places, double max, double offset)
198+ : _places(places), _max(max), _offset(offset) {
199 };
200 int formulaSize() const override{
201 return _places.size();
202 }
203 void analyze(AnalysisContext& context) override;
204+ size_t value(const MarkVal*);
205 Result evaluate(const EvaluationContext& context) override;
206 Result evalAndSet(const EvaluationContext& context) override;
207 uint32_t distance(DistanceContext& context) const override;
208@@ -1227,12 +1236,14 @@
209 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
210 void toXML(std::ostream&, uint32_t tabs) const override;
211 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
212- Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
213+ Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
214 Path getPath() const override { return Path::pError; }
215 CTLType getQueryType() const override { return CTLType::EVAL; }
216 bool containsNext() const override { return false; }
217 bool nestedDeadlock() const override { return false; }
218- size_t bounds() const { return _bound; }
219+ double bounds() const {
220+ return _offset + _bound;
221+ }
222 #ifdef ENABLE_TAR
223 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
224 #endif
225@@ -1243,8 +1254,8 @@
226 private:
227 std::vector<place_t> _places;
228 size_t _bound = 0;
229- size_t _max = std::numeric_limits<size_t>::max();
230-
231+ double _max = std::numeric_limits<double>::infinity();
232+ double _offset = 0;
233 };
234
235 }
236
237=== modified file 'PetriEngine/Reachability/ReachabilityResult.h'
238--- PetriEngine/Reachability/ReachabilityResult.h 2018-04-13 09:49:31 +0000
239+++ PetriEngine/Reachability/ReachabilityResult.h 2019-02-11 21:18:34 +0000
240@@ -73,7 +73,7 @@
241 const std::vector<size_t> enabledTransitionsCount = std::vector<size_t>(),
242 int maxTokens = 0,
243 const std::vector<uint32_t> maxPlaceBound = std::vector<uint32_t>(),
244- Structures::StateSetInterface* stateset = NULL, size_t lastmarking = 0 );
245+ Structures::StateSetInterface* stateset = NULL, size_t lastmarking = 0, const MarkVal* initialMarking = nullptr);
246
247 std::string printTechniques();
248
249
250=== modified file 'PetriEngine/Reachability/ReachabilitySearch.cpp'
251--- PetriEngine/Reachability/ReachabilitySearch.cpp 2018-05-12 15:14:12 +0000
252+++ PetriEngine/Reachability/ReachabilitySearch.cpp 2019-02-11 21:18:34 +0000
253@@ -69,7 +69,7 @@
254 return printer.printResult(i, query.get(), r,
255 ss.expandedStates, ss.exploredStates, states->discovered(),
256 ss.enabledTransitionsCount, states->maxTokens(),
257- states->maxPlaceBound(), states, _satisfyingMarking);
258+ states->maxPlaceBound(), states, _satisfyingMarking, _initial.marking());
259 }
260
261 void ReachabilitySearch::printStats(searchstate_t& ss, Structures::StateSetInterface* states)
262
263=== modified file 'PetriEngine/Reachability/ReachabilitySearch.h'
264--- PetriEngine/Reachability/ReachabilitySearch.h 2017-11-26 13:43:04 +0000
265+++ PetriEngine/Reachability/ReachabilitySearch.h 2019-02-11 21:18:34 +0000
266@@ -94,6 +94,7 @@
267 int _kbound;
268 PetriNet& _net;
269 size_t _satisfyingMarking = 0;
270+ Structures::State _initial;
271 };
272
273 template<typename Q, typename W, typename G>
274@@ -113,6 +114,7 @@
275 // set up working area
276 Structures::State state;
277 Structures::State working;
278+ _initial.setMarking(_net.makeInitialMarking());
279 state.setMarking(_net.makeInitialMarking());
280 working.setMarking(_net.makeInitialMarking());
281
282
283=== modified file 'PetriEngine/Reachability/ResultPrinter.cpp'
284--- PetriEngine/Reachability/ResultPrinter.cpp 2018-04-17 09:38:14 +0000
285+++ PetriEngine/Reachability/ResultPrinter.cpp 2019-02-11 21:18:34 +0000
286@@ -16,7 +16,8 @@
287 const std::vector<size_t> enabledTransitionsCount,
288 int maxTokens,
289 const std::vector<uint32_t> maxPlaceBound, Structures::StateSetInterface* stateset,
290- size_t lastmarking)
291+ size_t lastmarking,
292+ const MarkVal* initialMarking)
293 {
294 if(result == Unknown) return Unknown;
295
296@@ -24,7 +25,14 @@
297
298 if(options->cpnOverApprox)
299 {
300- if (result == Satisfied)
301+ if(query->getQuantifier() == PQL::Quantifier::UPPERBOUNDS)
302+ {
303+ auto upq = ((PQL::UnfoldedUpperBoundsCondition*)query);
304+ auto bnd = upq->bounds();
305+ if(initialMarking == nullptr || bnd > upq->value(initialMarking))
306+ retval = Unknown;
307+ }
308+ else if (result == Satisfied)
309 retval = query->isInvariant() ? Unknown : Unknown;
310 else if (result == NotSatisfied)
311 retval = query->isInvariant() ? Satisfied : NotSatisfied;
312
313=== modified file 'PetriEngine/Simplification/LinearProgram.cpp'
314--- PetriEngine/Simplification/LinearProgram.cpp 2017-12-11 08:24:36 +0000
315+++ PetriEngine/Simplification/LinearProgram.cpp 2019-02-11 21:18:34 +0000
316@@ -1,4 +1,5 @@
317 #include <assert.h>
318+#include <numeric>
319 #include "../../lpsolve/lp_lib.h"
320 #include "LinearProgram.h"
321 #include "LPCache.h"
322@@ -130,9 +131,17 @@
323
324 delete_lp(lp);
325
326- if (result == TIMEOUT) std::cout << "note: lpsolve timeout" << std::endl;
327- // Return true, if it was infeasible
328- if(result == INFEASIBLE)
329+ if(get_accuracy(lp) >= 0.5)
330+ {
331+ std::cout << "note: lpsolve had unacceptable accuracy" << std::endl;
332+ _result = result_t::POSSIBLE;
333+ }
334+ else if (result == TIMEOUT)
335+ {
336+ std::cout << "note: lpsolve timeout" << std::endl;
337+ _result = result_t::UKNOWN;
338+ }
339+ else if(result == INFEASIBLE)
340 {
341 _result = result_t::IMPOSSIBLE;
342 }
343@@ -142,6 +151,150 @@
344 }
345 return _result == result_t::IMPOSSIBLE;
346 }
347+
348+ std::vector<std::pair<double,bool>> LinearProgram::bounds(const PQL::SimplificationContext& context, uint32_t solvetime, const std::vector<uint32_t>& places)
349+ {
350+ std::vector<std::pair<double,bool>> result(places.size() + 1, std::make_pair(std::numeric_limits<double>::infinity(), false));
351+ auto net = context.net();
352+ auto m0 = context.marking();
353+ auto timeout = solvetime;
354+
355+ const uint32_t nCol = net->numberOfTransitions();
356+ const int nRow = net->numberOfPlaces();
357+ std::vector<REAL> row = std::vector<REAL>(nCol + 1);
358+ lprec* base_lp;
359+ {
360+ base_lp = make_lp(nRow, nCol);
361+ assert(base_lp);
362+ if (!base_lp) return result;
363+ set_verbose(base_lp, IMPORTANT);
364+
365+ set_add_rowmode(base_lp, TRUE);
366+
367+ int rowno = 1;
368+
369+ // restrict all places to contain 0+ tokens
370+ for (size_t p = 0; p < net->numberOfPlaces(); ++p) {
371+ memset(row.data(), 0, sizeof (REAL) * (nCol + 1));
372+ for (size_t t = 0; t < nCol; ++t) {
373+ row[1 + t] = net->outArc(t, p) - net->inArc(p, t);
374+ }
375+ set_row(base_lp, rowno, row.data());
376+ set_constr_type(base_lp, rowno, GE);
377+ set_rh(base_lp, rowno++, (0 - (int)m0[p]));
378+ }
379+
380+ set_add_rowmode(base_lp, FALSE);
381+ }
382+ for(size_t it = 0; it <= places.size(); ++it)
383+ {
384+ // we want to start with the overall bound, most important
385+ // Spend time on rest after
386+ size_t pi;
387+ if(it == 0)
388+ pi = places.size();
389+ else
390+ pi = it - 1;
391+
392+ if(context.timeout())
393+ {
394+ delete_lp(base_lp);
395+ return result;
396+ }
397+ // Create objective
398+ memset(row.data(), 0, sizeof (REAL) * net->numberOfTransitions() + 1);
399+ double p0 = 0;
400+ bool all_le_zero = true;
401+ bool all_zero = true;
402+ if(pi < places.size())
403+ {
404+ auto tp = places[pi];
405+ p0 = m0[tp];
406+ for (size_t t = 0; t < net->numberOfTransitions(); ++t)
407+ {
408+ row[1 + t] = net->outArc(t, tp) - net->inArc(tp, t);
409+ all_le_zero &= row[1 + t] <= 0;
410+ all_zero &= row[1 + t] == 0;
411+ }
412+ }
413+ else
414+ {
415+ for (size_t t = 0; t < net->numberOfTransitions(); ++t)
416+ {
417+ double cnt = 0;
418+ for(auto tp : places)
419+ cnt += net->outArc(t, tp) - net->inArc(tp, t);
420+ row[1 + t] = cnt;
421+ all_le_zero &= row[1 + t] <= 0;
422+ all_zero &= row[1 + t] == 0;
423+ }
424+ for(auto tp : places)
425+ p0 += m0[tp];
426+ }
427+
428+ if(all_le_zero)
429+ {
430+ result[pi].first = p0;
431+ result[pi].second = all_zero;
432+ if(pi == places.size())
433+ {
434+ delete_lp(base_lp);
435+ return result;
436+ }
437+ continue;
438+ }
439+
440+ // Set objective
441+ auto tmp_lp = copy_lp(base_lp);
442+ set_obj_fn(tmp_lp, row.data());
443+
444+ // Maximize
445+ set_maxim(tmp_lp);
446+
447+ for (size_t i = 0; i < nCol; i++){
448+ set_int(tmp_lp, 1 + i, TRUE);
449+ }
450+
451+ set_timeout(tmp_lp, timeout);
452+ set_presolve(tmp_lp, PRESOLVE_ROWS | PRESOLVE_COLS | PRESOLVE_LINDEP, get_presolveloops(tmp_lp));
453+ int res = solve(tmp_lp);
454+
455+ if(get_accuracy(tmp_lp) >= 0.5)
456+ {
457+ result[pi].first = (std::numeric_limits<double>::quiet_NaN());
458+ std::cout << "note: lpsolve had unacceptable accuracy" << std::endl;
459+ }
460+ else if (res == TIMEOUT)
461+ {
462+ result[pi].first = (std::numeric_limits<double>::quiet_NaN());
463+ std::cout << "note: lpsolve timeout" << std::endl;
464+ }
465+ else if(res == INFEASIBLE)
466+ {
467+ result[pi].first = p0;
468+ result[pi].second = all_zero;
469+ }
470+ else if(res == OPTIMAL)
471+ {
472+ result[pi].first = p0 + get_objective(tmp_lp);
473+ result[pi].second = all_zero;
474+ }
475+ delete_lp(tmp_lp);
476+ if(pi == places.size() && result[places.size()].first >= p0)
477+ {
478+ delete_lp(base_lp);
479+ return result;
480+ }
481+ if(pi == places.size() && places.size() == 1)
482+ {
483+ result[0] = result[1];
484+ delete_lp(base_lp);
485+ return result;
486+ }
487+ }
488+ delete_lp(base_lp);
489+ return result;
490+ }
491
492
493 void LinearProgram::make_union(const LinearProgram& other)
494
495=== modified file 'PetriEngine/Simplification/LinearProgram.h'
496--- PetriEngine/Simplification/LinearProgram.h 2017-12-11 08:24:36 +0000
497+++ PetriEngine/Simplification/LinearProgram.h 2019-02-11 21:18:34 +0000
498@@ -82,7 +82,7 @@
499 ss << "### LP DONE";
500 return ss;
501 }
502-
503+ static std::vector<std::pair<double,bool>> bounds(const PQL::SimplificationContext& context, uint32_t solvetime, const std::vector<uint32_t>& places);
504 };
505 }
506 }
507
508=== modified file 'PetriParse/QueryBinaryParser.cpp'
509--- PetriParse/QueryBinaryParser.cpp 2018-05-12 15:14:12 +0000
510+++ PetriParse/QueryBinaryParser.cpp 2019-02-11 21:18:34 +0000
511@@ -144,18 +144,22 @@
512 else if(q == Quantifier::UPPERBOUNDS)
513 {
514 uint32_t size;
515- size_t max;
516+ double max, offset;
517 binary.read(reinterpret_cast<char*>(&size), sizeof(uint32_t));
518- binary.read(reinterpret_cast<char*>(&max), sizeof(size_t));
519+ binary.read(reinterpret_cast<char*>(&max), sizeof(double));
520+ binary.read(reinterpret_cast<char*>(&offset), sizeof(double));
521 std::vector<UnfoldedUpperBoundsCondition::place_t> places;
522 for(size_t i = 0; i < size; ++i)
523 {
524 uint32_t id;
525+ double pmax;
526 binary.read(reinterpret_cast<char*>(&id), sizeof(uint32_t));
527+ binary.read(reinterpret_cast<char*>(&pmax), sizeof(double));
528 places.emplace_back(names[id]);
529 places.back()._place = id;
530+ places.back()._max = pmax;
531 }
532- return std::make_shared<UnfoldedUpperBoundsCondition>(places, max);
533+ return std::make_shared<UnfoldedUpperBoundsCondition>(places, max, offset);
534 }
535 else
536 {
537
538=== modified file 'VerifyPN.cpp'
539--- VerifyPN.cpp 2018-06-29 07:24:36 +0000
540+++ VerifyPN.cpp 2019-02-11 21:18:34 +0000
541@@ -715,7 +715,7 @@
542 negstat_t stats;
543 EvaluationContext context(nullptr, nullptr);
544 auto q = queries[qid]->pushNegation(stats, context, false, false, false);
545- if (!q->isReachability() || q->isLoopSensitive() || q->prepareForReachability()->getQuantifier() == UPPERBOUNDS || stats.negated_fireability) {
546+ if (!q->isReachability() || q->isLoopSensitive() || stats.negated_fireability) {
547 std::cerr << "Warning: CPN OverApproximation is only available for Reachability queries without deadlock, negated fireability and UpperBounds, skipping " << querynames[qid] << std::endl;
548 queries.erase(queries.begin() + qid);
549 querynames.erase(querynames.begin() + qid);
550
551=== modified file 'makefile.linux64'
552--- makefile.linux64 2018-04-17 12:09:54 +0000
553+++ makefile.linux64 2019-02-11 21:18:34 +0000
554@@ -6,7 +6,7 @@
555
556 # Compiler and linker flags
557 CFLAGS = -fPIC -flto -march=x86-64 -std=c++14 -m64 -I.
558-LDFLAGS = -flto=4 -march=x86-64 -std=c++14 -m64 -static lpsolve/liblpsolve55-linux64.a \
559+LDFLAGS = -flto=4 -march=x86-64 -std=c++14 -m64 lpsolve/liblpsolve55-linux64.a \
560 -static-libgcc -static-libstdc++
561 # -Wl,-Bstatic -ldl -lm -lc -Wl,-Bdynamic -lpthread
562

Subscribers

People subscribed via source and target branches