~verifypn-maintainers/verifypn/new-trunk : revision 252

3

* Thomas Søndersø Nielsen <primogens@gmail.com>,

4

* Lars Kærlund Østergaard <larsko@gmail.com>,

5

* Peter Gjøl Jensen <root@petergjoel.dk>

6

*

6

*

7

* This program is free software: you can redistribute it and/or modify

8

* it under the terms of the GNU General Public License as published by

9

* the Free Software Foundation, either version 3 of the License, or

10

* (at your option) any later version.

11

*

11

*

12

* This program is distributed in the hope that it will be useful,

13

* but WITHOUT ANY WARRANTY; without even the implied warranty of

14

* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the

15

* GNU General Public License for more details.

16

*

16

*

17

* You should have received a copy of the GNU General Public License

18

* along with this program. If not, see <http://www.gnu.org/licenses/>.

19

*/

38

39

namespace PetriEngine {

40

namespace PQL {

41

42

std::ostream& generateTabs(std::ostream& out, uint32_t tabs) {

43

44

for(uint32_t i = 0; i < tabs; i++) {

46

}

47

return out;

48

}

49

50

/** FOR COMPILING AND CONSTRUCTING LOGICAL OPERATORS **/

51

52

template<typename T>

61

_conds.emplace_back(ptr);

62

}

63

else if (auto comp = std::dynamic_pointer_cast<CompareCondition>(ptr))

64

{

64

{

65

if((std::is_same<T, AndCondition>::value && std::dynamic_pointer_cast<NotEqualCondition>(ptr)) ||

66

(std::is_same<T, OrCondition>::value && std::dynamic_pointer_cast<EqualCondition>(ptr)))

67

{

113

}

114

else

115

{

116

_conds.emplace_back(ptr);

116

_conds.emplace_back(ptr);

117

}

118

}

119

else

122

}

123

124

}

125

126

template<typename T, bool K>

127

Condition_ptr makeLog(const std::vector<Condition_ptr>& conds, bool aggressive)

128

{

138

return BooleanCondition::getShared(K);

139

return res;

140

}

141

142

Condition_ptr makeOr(const std::vector<Condition_ptr>& cptr)

141

142

Condition_ptr makeOr(const std::vector<Condition_ptr>& cptr)

143

{ return makeLog<OrCondition,false>(cptr, true); }

144

Condition_ptr makeAnd(const std::vector<Condition_ptr>& cptr)

144

Condition_ptr makeAnd(const std::vector<Condition_ptr>& cptr)

145

{ return makeLog<AndCondition,true>(cptr, true); }

146

Condition_ptr makeOr(const Condition_ptr& a, const Condition_ptr& b) {

147

std::vector<Condition_ptr> cnds{a,b};

148

return makeLog<OrCondition,false>(cnds, true);

149

}

150

Condition_ptr makeAnd(const Condition_ptr& a, const Condition_ptr& b)

151

{

152

std::vector<Condition_ptr> cnds{a,b};

153

return makeLog<AndCondition,true>(cnds, true);

154

}

155

156

146

Condition_ptr makeOr(const Condition_ptr& a, const Condition_ptr& b) {

147

std::vector<Condition_ptr> cnds{a,b};

148

return makeLog<OrCondition,false>(cnds, true);

149

}

150

Condition_ptr makeAnd(const Condition_ptr& a, const Condition_ptr& b)

151

{

152

std::vector<Condition_ptr> cnds{a,b};

153

return makeLog<AndCondition,true>(cnds, true);

154

}

155

156

157

// CONSTANTS

158

Condition_ptr BooleanCondition::FALSE_CONSTANT = std::make_shared<BooleanCondition>(false);

159

Condition_ptr BooleanCondition::TRUE_CONSTANT = std::make_shared<BooleanCondition>(true);

160

Condition_ptr DeadlockCondition::DEADLOCK = std::make_shared<DeadlockCondition>();

161

162

161

162

163

Condition_ptr BooleanCondition::getShared(bool val)

164

{

165

if(val)

178

out << op() << " ";

179

_cond->toTAPAALQuery(out,context);

180

}

181

182

void UntilCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {

183

out << op() << " (";

184

_cond1->toTAPAALQuery(out, context);

186

_cond2->toTAPAALQuery(out,context);

187

out << ")";

188

}

189

190

void LogicalCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {

191

out << "(";

192

_conds[0]->toTAPAALQuery(out, context);

197

}

198

out << ")";

199

}

200

201

void CompareConjunction::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {

202

out << "(";

203

if(_negated) out << "!";

205

for(auto& c : _constraints)

206

{

207

if(!first) out << " and ";

208

if(c._lower != 0)

208

if(c._lower != 0)

209

out << "(" << c._lower << " <= " << context.netName << "." << c._name << ")";

210

if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max())

210

if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max())

211

out << " and ";

212

if(c._lower != 0)

212

if(c._lower != 0)

213

out << "(" << c._upper << " >= " << context.netName << "." << c._name << ")";

214

first = false;

215

}

270

}

271

out << ")";

272

}

273

274

/******************** opTAPAAL ********************/

275

276

std::string EqualCondition::opTAPAAL() const {

405

void SimpleQuantifierCondition::analyze(AnalysisContext& context) {

406

_cond->analyze(context);

407

}

408

409

void UntilCondition::analyze(AnalysisContext& context) {

410

_cond1->analyze(context);

411

_cond2->analyze(context);

412

}

413

414

void LogicalCondition::analyze(AnalysisContext& context) {

415

for(auto& c : _conds) c->analyze(context);

416

}

417

418

void UnfoldedFireableCondition::_analyze(AnalysisContext& context)

419

{

420

std::vector<Condition_ptr> conds;

425

_name.length());

426

context.reportError(error);

427

return;

428

}

428

}

429

430

assert(_name.compare(context.net()->transitionNames()[result.offset]) == 0);

431

auto preset = context.net()->preset(result.offset);

462

ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());

463

coloredContext->reportError(error);

464

return;

465

}

465

}

466

if(names.size() < 1){

467

//If the transition points to empty vector we know that it has

467

//If the transition points to empty vector we know that it has

468

//no legal bindings and can never fire

469

_compiled = std::make_shared<BooleanCondition>(false);

470

_compiled->analyze(context);

497

_expr1->analyze(context);

498

_expr2->analyze(context);

499

}

500

501

void NotCondition::analyze(AnalysisContext& context) {

502

_cond->analyze(context);

503

}

639

}

640

_compiled->analyze(context);

641

}

642

643

void UnfoldedUpperBoundsCondition::analyze(AnalysisContext& c)

644

{

645

for(auto& p : _places)

833

setUpperBound(value(context.marking()));

834

return _max <= _bound ? RTRUE : RUNKNOWN;

835

}

836

837

/******************** Evaluation - save result ********************/

838

Condition::Result SimpleQuantifierCondition::evalAndSet(const EvaluationContext& context) {

839

return RUNKNOWN;

880

setSatisfied(res);

881

return res;

882

}

883

884

Condition::Result UntilCondition::evalAndSet(const EvaluationContext& context) {

885

auto r2 = _cond2->evalAndSet(context);

886

if(r2 != RFALSE) return r2;

887

auto r1 = _cond1->evalAndSet(context);

888

if(r1 == RFALSE) return RFALSE;

889

return RUNKNOWN;

890

}

890

}

891

892

int Expr::evalAndSet(const EvaluationContext& context) {

893

int r = evaluate(context);

939

setSatisfied(res);

940

return res;

941

}

942

943

Condition::Result CompareCondition::evalAndSet(const EvaluationContext& context) {

944

int v1 = _expr1->evalAndSet(context);

945

int v2 = _expr2->evalAndSet(context);

966

setSatisfied(context.net()->deadlocked(context.marking()));

967

return isSatisfied() ? RTRUE : RFALSE;

968

}

969

970

Condition::Result UnfoldedUpperBoundsCondition::evalAndSet(const EvaluationContext& context)

971

{

972

auto res = evaluate(context);

990

{

991

ctx.accept<decltype(this)>(this);

992

}

993

994

void EXCondition::visit(Visitor& ctx) const

995

{

996

ctx.accept<decltype(this)>(this);

997

}

998

999

void EFCondition::visit(Visitor& ctx) const

1000

{

1001

ctx.accept<decltype(this)>(this);

1004

void AUCondition::visit(Visitor& ctx) const

1005

{

1006

ctx.accept<decltype(this)>(this);

1007

}

1007

}

1008

1009

void AXCondition::visit(Visitor& ctx) const

1010

{

1014

void AFCondition::visit(Visitor& ctx) const

1015

{

1016

ctx.accept<decltype(this)>(this);

1017

}

1017

}

1018

1019

void AGCondition::visit(Visitor& ctx) const

1020

{

1060

{

1061

ctx.accept<decltype(this)>(this);

1062

}

1063

1064

void EqualCondition::visit(Visitor& ctx) const

1065

{

1066

ctx.accept<decltype(this)>(this);

1075

{

1076

ctx.accept<decltype(this)>(this);

1077

}

1078

1079

void LessThanOrEqualCondition::visit(Visitor& ctx) const

1080

{

1081

ctx.accept<decltype(this)>(this);

1082

}

1083

1084

void LessThanCondition::visit(Visitor& ctx) const

1085

{

1086

ctx.accept<decltype(this)>(this);

1087

}

1088

1089

void BooleanCondition::visit(Visitor& ctx) const

1090

{

1091

ctx.accept<decltype(this)>(this);

1092

}

1093

1094

void DeadlockCondition::visit(Visitor& ctx) const

1095

{

1096

ctx.accept<decltype(this)>(this);

1143

else

1144

ctx.accept<decltype(this)>(this);

1145

}

1146

1147

void UnfoldedFireableCondition::visit(Visitor& ctx) const

1148

{

1149

if(_compiled)

1152

ctx.accept<decltype(this)>(this);

1153

}

1154

1155

1156

void UnfoldedUpperBoundsCondition::visit(Visitor& ctx) const

1157

{

1158

ctx.accept<decltype(this)>(this);

1159

}

1160

1161

void LiteralExpr::visit(Visitor& ctx) const

1162

{

1163

ctx.accept<decltype(this)>(this);

1393

int MultiplyExpr::apply(int v1, int v2) const {

1394

return v1 * v2;

1395

}

1396

1397

/******************** Apply (CompareCondition subclasses) ********************/

1398

1399

bool EqualCondition::apply(int v1, int v2) const {

1425

std::string MultiplyExpr::op() const {

1426

return "*";

1427

}

1428

1429

/******************** Op (QuantifierCondition subclasses) ********************/

1430

1431

std::string ACondition::op() const {

1447

std::string XCondition::op() const {

1448

return "X";

1449

}

1450

1451

std::string EXCondition::op() const {

1452

return "EX";

1453

}

1454

1455

std::string EGCondition::op() const {

1456

return "EG";

1457

}

1458

1459

std::string EFCondition::op() const {

1460

return "EF";

1461

}

1462

1463

std::string AXCondition::op() const {

1464

return "AX";

1465

}

1466

1467

std::string AGCondition::op() const {

1468

return "AG";

1469

}

1470

1471

std::string AFCondition::op() const {

1472

return "AF";

1473

}

1481

std::string EUCondition::op() const {

1482

return "E";

1483

}

1484

1485

std::string AUCondition::op() const {

1486

return "A";

1487

}

1488

1489

/******************** Op (LogicalCondition subclasses) ********************/

1490

1491

std::string AndCondition::op() const {

1514

return "<=";

1515

}

1516

1517

/******************** free of places ********************/

1517

/******************** free of places ********************/

1518

1519

bool NaryExpr::placeFree() const

1520

{

1523

return false;

1524

return true;

1525

}

1526

1527

bool CommutativeExpr::placeFree() const

1528

{

1529

if(_ids.size() > 0) return false;

1530

return NaryExpr::placeFree();

1531

}

1532

1533

bool MinusExpr::placeFree() const

1534

{

1535

return _expr->placeFree();

1536

}

1537

1538

/******************** Expr::type() implementation ********************/

1539

1540

Expr::Types PlusExpr::type() const {

1610

return 0;

1611

}

1612

1613

uint32_t UnfoldedUpperBoundsCondition::distance(DistanceContext& context) const

1613

uint32_t UnfoldedUpperBoundsCondition::distance(DistanceContext& context) const

1614

{

1615

size_t tmp = 0;

1616

for(auto& p : _places)

1617

{

1618

tmp += context.marking()[p._place];

1619

}

1620

1621

return _max - tmp;

1622

}

1623

1624

uint32_t EFCondition::distance(DistanceContext& context) const {

1625

return _cond->distance(context);

1626

}

1636

uint32_t EUCondition::distance(DistanceContext& context) const {

1637

return _cond2->distance(context);

1638

}

1639

1640

uint32_t AFCondition::distance(DistanceContext& context) const {

1641

context.negate();

1642

uint32_t retval = _cond->distance(context);

1643

context.negate();

1644

return retval;

1645

}

1646

1647

uint32_t AXCondition::distance(DistanceContext& context) const {

1648

context.negate();

1649

uint32_t retval = _cond->distance(context);

1665

context.negate();

1666

return r1 + r2;

1667

}

1668

1669

uint32_t CompareConjunction::distance(DistanceContext& context) const {

1670

uint32_t d = 0;

1671

auto neg = context.negated() != _negated;

1691

else d = std::min(d, d2);

1692

first = false;

1693

}

1694

1695

if(c._lower != 0)

1696

{

1697

auto d2 = delta<LessThanOrEqualCondition>(c._upper, pv, neg);

1739

int d;

1740

unsigned int p;

1741

};

1742

1743

uint32_t LessThanOrEqualCondition::distance(DistanceContext& context) const {

1744

return _distance(context, delta<LessThanOrEqualCondition>);

1745

}

1746

1747

uint32_t LessThanCondition::distance(DistanceContext& context) const {

1748

return _distance(context, delta<LessThanCondition>);

1749

}

1750

1751

uint32_t NotEqualCondition::distance(DistanceContext& context) const {

1752

return _distance(context, delta<NotEqualCondition>);

1753

}

1754

1755

uint32_t EqualCondition::distance(DistanceContext& context) const {

1756

return _distance(context, delta<EqualCondition>);

1757

}

1758

1759

/******************** BIN output ********************/

1760

1761

void LiteralExpr::toBinary(std::ostream& out) const {

1762

out.write("l", sizeof(char));

1763

out.write(reinterpret_cast<const char*>(&_value), sizeof(int));

1764

}

1765

1766

void UnfoldedIdentifierExpr::toBinary(std::ostream& out) const {

1767

out.write("i", sizeof(char));

1768

out.write(reinterpret_cast<const char*>(&_offsetInMarking), sizeof(int));

1768

out.write(reinterpret_cast<const char*>(&_offsetInMarking), sizeof(int));

1769

}

1770

1771

void MinusExpr::toBinary(std::ostream& out) const

1772

{

1773

auto e1 = std::make_shared<PQL::LiteralExpr>(0);

1776

exprs.push_back(_expr);

1777

PQL::SubtractExpr(std::move(exprs)).toBinary(out);

1778

}

1779

1780

void SubtractExpr::toBinary(std::ostream& out) const {

1781

out.write("-", sizeof(char));

1782

uint32_t size = _exprs.size();

1799

for(auto& e : _exprs)

1800

e->toBinary(out);

1801

}

1802

1803

void SimpleQuantifierCondition::toBinary(std::ostream& out) const

1804

{

1805

auto path = getPath();

1818

_cond1->toBinary(out);

1819

_cond2->toBinary(out);

1820

}

1821

1822

void LogicalCondition::toBinary(std::ostream& out) const

1823

{

1824

auto path = getPath();

1829

out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));

1830

for(auto& c : _conds) c->toBinary(out);

1831

}

1832

1833

void CompareConjunction::toBinary(std::ostream& out) const

1834

{

1835

auto path = getPath();

1841

out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));

1842

for(auto& c : _constraints)

1843

{

1844

out.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));

1844

out.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));

1845

out.write(reinterpret_cast<const char*>(&c._lower), sizeof(uint32_t));

1846

out.write(reinterpret_cast<const char*>(&c._upper), sizeof(uint32_t));

1847

}

1848

}

1849

1850

void CompareCondition::toBinary(std::ostream& out) const

1851

{

1852

auto path = getPath();

1859

_expr1->toBinary(out);

1860

_expr2->toBinary(out);

1861

}

1862

1863

void DeadlockCondition::toBinary(std::ostream& out) const

1864

{

1865

auto path = getPath();

1867

out.write(reinterpret_cast<const char*>(&path), sizeof(Path));

1868

out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));

1869

}

1870

1871

void BooleanCondition::toBinary(std::ostream& out) const

1872

{

1873

auto path = getPath();

1876

out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));

1877

out.write(reinterpret_cast<const char*>(&value), sizeof(bool));

1878

}

1879

1880

void UnfoldedUpperBoundsCondition::toBinary(std::ostream& out) const

1881

{

1882

auto path = getPath();

1883

auto quant = Quantifier::UPPERBOUNDS;

1884

out.write(reinterpret_cast<const char*>(&path), sizeof(Path));

1885

out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));

1885

out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));

1886

uint32_t size = _places.size();

1887

out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));

1888

out.write(reinterpret_cast<const char*>(&_max), sizeof(double));

1889

out.write(reinterpret_cast<const char*>(&_offset), sizeof(double));

1887

out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));

1888

out.write(reinterpret_cast<const char*>(&_max), sizeof(double));

1889

out.write(reinterpret_cast<const char*>(&_offset), sizeof(double));

1890

for(auto& b : _places)

1891

{

1892

out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));

1892

out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));

1893

out.write(reinterpret_cast<const char*>(&b._max), sizeof(double));

1894

}

1895

}

1896

1897

void NotCondition::toBinary(std::ostream& out) const

1898

{

1899

auto path = getPath();

1902

out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));

1903

_cond->toBinary(out);

1904

}

1905

1906

/******************** CTL Output ********************/

1907

1905

1906

/******************** CTL Output ********************/

1907

1908

void LiteralExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {

1909

generateTabs(out,tabs) << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";

1910

}

1929

ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());

1930

coloredContext->reportError(error);

1931

return;

1932

}

1932

}

1933

if(names.size() < 1){

1934

//If the transition points to empty vector we know that it has

1934

//If the transition points to empty vector we know that it has

1935

//no legal bindings and can never fire

1936

out << "<false/>";

1937

return;

1938

}

1939

1940

out << "<is-fireable>";

1941

for (auto& unfoldedName : names) {

1942

out << "<transition>" + unfoldedName << "</transition>";

1944

out << "</is-fireable>";

1945

}

1946

}

1947

1948

void UnfoldedIdentifierExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {

1949

if (tokencount) {

1950

generateTabs(out,tabs) << "<place>" << _name << "</place>\n";

1951

}

1952

else

1953

{

1954

generateTabs(out,tabs) << "<tokens-count>\n";

1954

generateTabs(out,tabs) << "<tokens-count>\n";

1955

generateTabs(out,tabs+1) << "<place>" << _name << "</place>\n";

1956

generateTabs(out,tabs) << "</tokens-count>\n";

1957

}

1963

}

1964

else

1965

{

1966

out << "<tokens-count>\n";

1966

out << "<tokens-count>\n";

1967

out << "<place>" << _name << "</place>\n";

1968

out << "</tokens-count>\n";

1969

}

1977

ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());

1978

coloredContext->reportError(error);

1979

return;

1980

}

1981

1982

1980

}

1981

1982

1983

out << "<tokens-count>\n";

1984

for (auto& unfoldedName : names) {

1985

out << "<place>" << unfoldedName.second << "</place>\n";

1991

}

1992

else

1993

{

1994

out << "<tokens-count>\n";

1994

out << "<tokens-count>\n";

1995

out << "<place>" << _name << "</place>\n";

1996

out << "</tokens-count>\n";

1997

}

1998

}

1999

}

2000

2001

void PlusExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {

2002

if (tokencount) {

2003

for(auto& e : _exprs) e->toXML(ss,tabs, tokencount);

2004

return;

2005

}

2006

2007

if(tk) {

2008

generateTabs(ss,tabs) << "<tokens-count>\n";

2009

for(auto& e : _ids) generateTabs(ss,tabs+1) << "<place>" << e.second << "</place>\n";

2015

generateTabs(ss,tabs+1) << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";

2016

for(auto& i : _ids)

2017

{

2018

generateTabs(ss,tabs+1) << "<tokens-count>\n";

2018

generateTabs(ss,tabs+1) << "<tokens-count>\n";

2019

generateTabs(ss,tabs+2) << "<place>" << i.second << "</place>\n";

2020

generateTabs(ss,tabs+1) << "</tokens-count>\n";

2020

generateTabs(ss,tabs+1) << "</tokens-count>\n";

2021

}

2022

for(auto& e : _exprs) e->toXML(ss,tabs+1, tokencount);

2023

generateTabs(ss,tabs) << "</integer-sum>\n";

2028

for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);

2029

return;

2030

}

2031

2032

if(tk) {

2033

out << "<tokens-count>\n";

2034

for(auto& e : _ids) out << "<place>" << e.second << "</place>\n";

2040

out << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";

2041

for(auto& i : _ids)

2042

{

2043

out << "<tokens-count>\n";

2043

out << "<tokens-count>\n";

2044

out << "<place>" << i.second << "</place>\n";

2045

out << "</tokens-count>\n";

2045

out << "</tokens-count>\n";

2046

}

2047

for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);

2048

out << "</integer-sum>\n";

2049

}

2050

2051

void SubtractExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {

2052

generateTabs(ss,tabs) << "<integer-difference>\n";

2053

for(auto& e : _exprs) e->toXML(ss,tabs+1);

2059

for(auto& e : _exprs) e->toCompactXML(out,tabs, context);

2060

out << "</integer-difference>\n";

2061

}

2062

2063

void MultiplyExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {

2064

generateTabs(ss,tabs) << "<integer-product>\n";

2065

for(auto& e : _exprs) e->toXML(ss,tabs+1);

2071

for(auto& e : _exprs) e->toCompactXML(out,tabs, context);

2072

out << "</integer-product>\n";

2073

}

2074

2075

void MinusExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {

2076

2077

generateTabs(out,tabs) << "<integer-product>\n";

2078

_expr->toXML(out,tabs+1);

2079

generateTabs(out,tabs+1) << "<integer-difference>\n" ; generateTabs(out,tabs+2) <<

2080

"<integer-constant>0</integer-constant>\n" ; generateTabs(out,tabs+2) <<

2080

"<integer-constant>0</integer-constant>\n" ; generateTabs(out,tabs+2) <<

2081

"<integer-constant>1</integer-constant>\n" ; generateTabs(out,tabs+1) <<

2082

"</integer-difference>\n" ; generateTabs(out,tabs) << "</integer-product>\n";

2083

}

2086

out << "<integer-product>\n";

2087

_expr->toCompactXML(out,tabs, context);

2088

out << "<integer-difference>\n" ; out <<

2089

"<integer-constant>0</integer-constant>\n" ; out <<

2089

"<integer-constant>0</integer-constant>\n" ; out <<

2090

"<integer-constant>1</integer-constant>\n" ; out <<

2091

"</integer-difference>\n" ; out << "</integer-product>\n";

2092

}

2093

2094

void EXCondition::toXML(std::ostream& out,uint32_t tabs) const {

2095

generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<next>\n";

2096

_cond->toXML(out,tabs+2);

2103

out << "</next>\n" ; out << "</exists-path>\n";

2104

}

2105

2106

void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {

2106

void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {

2107

generateTabs(out,tabs) << "<all-paths>\n"; generateTabs(out,tabs+1) << "<next>\n";

2108

_cond->toXML(out,tabs+2);

2108

_cond->toXML(out,tabs+2);

2109

generateTabs(out,tabs+1) << "</next>\n"; generateTabs(out,tabs) << "</all-paths>\n";

2110

}

2111

2112

void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2112

void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2113

out << "<all-paths>\n" ;out << "<next>\n";

2114

_cond->toCompactXML(out,tabs+2, context);

2115

out << "</next>\n" ; out << "</all-paths>\n";

2116

}

2117

2118

void EFCondition::toXML(std::ostream& out,uint32_t tabs) const {

2119

generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<finally>\n";

2120

_cond->toXML(out,tabs+2);

2121

generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";

2122

}

2123

2124

void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2124

void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2125

out << "<exists-path>\n" ;out << "<finally>\n";

2126

_cond->toCompactXML(out,tabs+2, context);

2127

out << "</finally>\n" ; out << "</exists-path>\n";

2128

}

2129

2130

void AFCondition::toXML(std::ostream& out,uint32_t tabs) const {

2131

generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<finally>\n";

2132

_cond->toXML(out,tabs+2);

2133

generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";

2134

}

2135

2136

void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2136

void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2137

out << "<all-paths>\n" ;out << "<finally>\n";

2138

_cond->toCompactXML(out,tabs+2, context);

2139

out << "</finally>\n" ; out << "</all-paths>\n";

2140

}

2141

2142

void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {

2141

2142

void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {

2143

generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<globally>\n";

2144

_cond->toXML(out,tabs+2);

2144

_cond->toXML(out,tabs+2);

2145

generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";

2146

}

2147

2148

void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2148

void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2149

out << "<exists-path>\n" ;out << "<globally>\n";

2150

_cond->toCompactXML(out,tabs+2, context);

2151

out << "</globally>\n" ; out << "</exists-path>\n";

2152

}

2153

2154

void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {

2153

2154

void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {

2155

generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<globally>\n";

2156

_cond->toXML(out,tabs+2);

2157

generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";

2158

}

2159

2160

void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2160

void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2161

out << "<all-paths>\n" ;out << "<globally>\n";

2162

_cond->toCompactXML(out,tabs+2, context);

2163

out << "</globally>\n" ; out << "</all-paths>\n";

2164

}

2165

2166

void EUCondition::toXML(std::ostream& out,uint32_t tabs) const {

2167

generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";

2168

_cond1->toXML(out,tabs+3);

2171

generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</exists-path>\n";

2172

}

2173

2174

void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2174

void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2175

out << "<exists-path>\n" ; out << "<until>\n" ; out << "<before>\n";

2176

_cond1->toCompactXML(out,tabs+2, context);

2177

out << "</before>\n" ; out << "<reach>\n";

2178

_cond2->toCompactXML(out,tabs+2, context);

2179

out << "</reach>\n" ; out << "</until>\n" ; out << "</exists-path>\n";

2180

}

2181

2182

void AUCondition::toXML(std::ostream& out,uint32_t tabs) const {

2183

generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";

2184

_cond1->toXML(out,tabs+3);

2187

generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";

2188

}

2189

2190

void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2190

void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2191

out << "<all-paths>\n" ; out << "<until>\n" ; out << "<before>\n";

2192

_cond1->toCompactXML(out,tabs+2, context);

2193

out << "</before>\n" ; out << "<reach>\n";

2201

generateTabs(out, tabs) << "</all-paths>\n";

2202

}

2203

2204

void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2204

void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2205

out << "<all-paths>\n" ;

2206

_cond->toCompactXML(out,tabs+2, context);

2207

out << "</all-paths>\n";

2213

generateTabs(out, tabs) << "</exists-path>\n";

2214

}

2215

2216

void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2216

void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2217

out << "<exists-path>\n" ;

2218

_cond->toCompactXML(out,tabs+2, context);

2219

out << "</exists-path>\n";

2225

generateTabs(out, tabs) << "</finally>\n";

2226

}

2227

2228

void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2228

void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2229

out << "<finally>\n" ;

2230

_cond->toCompactXML(out,tabs+2, context);

2231

out << "</finally>\n";

2237

generateTabs(out, tabs) << "</globally>\n";

2238

}

2239

2240

void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2240

void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2241

out << "<globally>\n" ;

2242

_cond->toCompactXML(out,tabs+2, context);

2243

out << "</globally>\n";

2249

generateTabs(out, tabs) << "</next>\n";

2250

}

2251

2252

void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2252

void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2253

out << "<next>\n" ;

2254

_cond->toCompactXML(out,tabs+2, context);

2255

out << "</next>\n";

2263

generateTabs(out,tabs+1) << "</reach>\n" ; generateTabs(out,tabs) << "</until>\n" ;

2264

}

2265

2266

void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2266

void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2267

out << "<until>\n" ; out << "<before>\n";

2268

_cond1->toCompactXML(out,tabs+2, context);

2269

out << "</before>\n" ; out << "<reach>\n";

2298

}

2299

for(size_t i = _conds.size() - 1; i > 1; --i)

2300

{

2301

generateTabs(out,tabs + i) << "</conjunction>\n";

2301

generateTabs(out,tabs + i) << "</conjunction>\n";

2302

}

2303

generateTabs(out,tabs) << "</conjunction>\n";

2303

generateTabs(out,tabs) << "</conjunction>\n";

2304

}

2305

2306

void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2306

void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2307

if(_conds.size() == 0)

2308

{

2309

BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);

2330

}

2331

for(size_t i = _conds.size() - 1; i > 1; --i)

2332

{

2333

out << "</conjunction>\n";

2333

out << "</conjunction>\n";

2334

}

2335

out << "</conjunction>\n";

2335

out << "</conjunction>\n";

2336

}

2337

2338

void OrCondition::toXML(std::ostream& out,uint32_t tabs) const {

2339

if(_conds.size() == 0)

2340

{

2362

}

2363

for(size_t i = _conds.size() - 1; i > 1; --i)

2364

{

2365

generateTabs(out,tabs + i) << "</disjunction>\n";

2365

generateTabs(out,tabs + i) << "</disjunction>\n";

2366

}

2367

generateTabs(out,tabs) << "</disjunction>\n";

2367

generateTabs(out,tabs) << "</disjunction>\n";

2368

}

2369

2370

void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2370

void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2371

if(_conds.size() == 0)

2372

{

2373

BooleanCondition::FALSE_CONSTANT->toCompactXML(out,tabs, context);

2394

}

2395

for(size_t i = _conds.size() - 1; i > 1; --i)

2396

{

2397

out << "</disjunction>\n";

2397

out << "</disjunction>\n";

2398

}

2399

out << "</disjunction>\n";

2399

out << "</disjunction>\n";

2400

}

2401

2402

void CompareConjunction::toXML(std::ostream& out, uint32_t tabs) const

2405

if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toXML(out, tabs);

2406

else

2407

{

2408

bool single = _constraints.size() == 1 &&

2408

bool single = _constraints.size() == 1 &&

2409

(_constraints[0]._lower == 0 ||

2410

_constraints[0]._upper == std::numeric_limits<uint32_t>::max());

2411

if(!single)

2411

if(!single)

2412

generateTabs(out,tabs) << "<conjunction>\n";

2413

for(auto& c : _constraints)

2414

{

2419

generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";

2420

generateTabs(out,tabs+2) << "</tokens-count>\n";

2421

generateTabs(out,tabs+2) << "<integer-constant>" << c._lower << "</integer-constant>\n";

2422

generateTabs(out,tabs+1) << "</integer-ge>\n";

2422

generateTabs(out,tabs+1) << "</integer-ge>\n";

2423

}

2424

if(c._upper != std::numeric_limits<uint32_t>::max())

2425

{

2428

generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";

2429

generateTabs(out,tabs+2) << "</tokens-count>\n";

2430

generateTabs(out,tabs+2) << "<integer-constant>" << c._upper << "</integer-constant>\n";

2431

generateTabs(out,tabs+1) << "</integer-le>\n";

2431

generateTabs(out,tabs+1) << "</integer-le>\n";

2432

}

2433

}

2434

if(!single)

2437

if(_negated) generateTabs(out,--tabs) << "</negation>";

2438

}

2439

2440

void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2440

void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2441

if(_negated) out << "<negation>";

2442

if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);

2443

else

2444

{

2445

bool single = _constraints.size() == 1 &&

2445

bool single = _constraints.size() == 1 &&

2446

(_constraints[0]._lower == 0 ||

2447

_constraints[0]._upper == std::numeric_limits<uint32_t>::max());

2448

if(!single)

2448

if(!single)

2449

out << "<conjunction>\n";

2450

for(auto& c : _constraints)

2451

{

2456

out << "<place>" << c._name << "</place>\n";

2457

out << "</tokens-count>\n";

2458

out << "<integer-constant>" << c._lower << "</integer-constant>\n";

2459

out << "</integer-ge>\n";

2459

out << "</integer-ge>\n";

2460

}

2461

if(c._upper != std::numeric_limits<uint32_t>::max())

2462

{

2465

out << "<place>" << c._name << "</place>\n";

2466

out << "</tokens-count>\n";

2467

out << "<integer-constant>" << c._upper << "</integer-constant>\n";

2468

out << "</integer-le>\n";

2468

out << "</integer-le>\n";

2469

}

2470

}

2471

if(!single)

2472

out << "</conjunction>\n";

2473

}

2474

if(_negated) out << "</negation>";

2474

if(_negated) out << "</negation>";

2475

}

2476

2477

void EqualCondition::toXML(std::ostream& out,uint32_t tabs) const {

2478

generateTabs(out,tabs) << "<integer-eq>\n";

2479

_expr1->toXML(out,tabs+1);

2480

_expr2->toXML(out,tabs+1);

2481

generateTabs(out,tabs) << "</integer-eq>\n";

2481

generateTabs(out,tabs) << "</integer-eq>\n";

2482

}

2483

2484

void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2484

void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2485

out << "<integer-eq>\n";

2486

_expr1->toCompactXML(out,tabs, context);

2487

_expr2->toCompactXML(out,tabs, context);

2488

out << "</integer-eq>\n";

2489

}

2490

2491

void NotEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {

2492

generateTabs(out,tabs) << "<integer-ne>\n";

2493

_expr1->toXML(out,tabs+1);

2494

_expr2->toXML(out,tabs+1);

2495

generateTabs(out,tabs) << "</integer-ne>\n";

2495

generateTabs(out,tabs) << "</integer-ne>\n";

2496

}

2497

2498

void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2498

void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2499

out << "<integer-ne>\n";

2500

_expr1->toCompactXML(out,tabs, context);

2501

_expr2->toCompactXML(out,tabs, context);

2502

out << "</integer-ne>\n";

2503

}

2504

2505

void LessThanCondition::toXML(std::ostream& out,uint32_t tabs) const {

2506

generateTabs(out,tabs) << "<integer-lt>\n";

2507

_expr1->toXML(out,tabs+1);

2508

_expr2->toXML(out,tabs+1);

2509

generateTabs(out,tabs) << "</integer-lt>\n";

2509

generateTabs(out,tabs) << "</integer-lt>\n";

2510

}

2511

2512

void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2512

void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2513

out << "<integer-lt>\n";

2514

_expr1->toCompactXML(out,tabs, context);

2515

_expr2->toCompactXML(out,tabs, context);

2516

out << "</integer-lt>\n";

2517

}

2518

2519

void LessThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {

2520

generateTabs(out,tabs) << "<integer-le>\n";

2521

_expr1->toXML(out,tabs+1);

2522

_expr2->toXML(out,tabs+1);

2523

generateTabs(out,tabs) << "</integer-le>\n";

2523

generateTabs(out,tabs) << "</integer-le>\n";

2524

}

2525

2526

void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2526

void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2527

out << "<integer-le>\n";

2528

_expr1->toCompactXML(out,tabs, context);

2529

_expr2->toCompactXML(out,tabs, context);

2530

out << "</integer-le>\n";

2531

}

2532

2533

void NotCondition::toXML(std::ostream& out,uint32_t tabs) const {

2534

2535

generateTabs(out,tabs) << "<negation>\n";

2536

_cond->toXML(out,tabs+1);

2537

generateTabs(out,tabs) << "</negation>\n";

2537

generateTabs(out,tabs) << "</negation>\n";

2538

}

2539

2540

void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2540

void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2541

out << "<negation>\n";

2542

_cond->toCompactXML(out,tabs, context);

2543

out << "</negation>\n";

2544

}

2545

2546

void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {

2547

generateTabs(out,tabs) << "<" <<

2548

(value ? "true" : "false")

2549

<< "/>\n";

2550

}

2551

2552

void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2553

out << "<" <<

2554

(value ? "true" : "false")

2555

<< "/>\n";

2556

}

2557

2545

2546

void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {

2547

generateTabs(out,tabs) << "<" <<

2548

(value ? "true" : "false")

2549

<< "/>\n";

2550

}

2551

2552

void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2553

out << "<" <<

2554

(value ? "true" : "false")

2555

<< "/>\n";

2556

}

2557

2558

void DeadlockCondition::toXML(std::ostream& out,uint32_t tabs) const {

2559

generateTabs(out,tabs) << "<deadlock/>\n";

2559

generateTabs(out,tabs) << "<deadlock/>\n";

2560

}

2561

2562

void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2562

void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2563

out << "<deadlock/>\n";

2564

}

2565

2566

void UnfoldedUpperBoundsCondition::toXML(std::ostream& out, uint32_t tabs) const {

2567

generateTabs(out, tabs) << "<place-bound>\n";

2568

for(auto& p : _places)

2570

generateTabs(out, tabs) << "</place-bound>\n";

2571

}

2572

2573

void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2573

void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{

2574

out << "<place-bound>\n";

2575

for(auto& p : _places)

2576

out << "<place>" << p._name << "</place>\n";

2577

out << "</place-bound>\n";

2577

out << "</place-bound>\n";

2578

}

2579

2580

/******************** Query Simplification ********************/

2581

2579

2580

/******************** Query Simplification ********************/

2581

2582

Member LiteralExpr::constraint(SimplificationContext& context) const {

2583

return Member(_value);

2584

}

2585

2586

Member memberForPlace(size_t p, SimplificationContext& context)

2585

2586

Member memberForPlace(size_t p, SimplificationContext& context)

2587

{

2588

std::vector<int> row(context.net()->numberOfTransitions(), 0);

2589

row.shrink_to_fit();

2590

for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) {

2591

row[t] = context.net()->outArc(t, p) - context.net()->inArc(p, t);

2592

}

2593

return Member(std::move(row), context.marking()[p]);

2593

return Member(std::move(row), context.marking()[p]);

2594

}

2595

2596

Member UnfoldedIdentifierExpr::constraint(SimplificationContext& context) const {

2597

return memberForPlace(_offsetInMarking, context);

2598

}

2599

2600

Member CommutativeExpr::commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const

2601

{

2602

Member res;

2606

first = false;

2607

res = Member(_constant);

2608

}

2609

2610

for(auto& i : _ids)

2611

{

2612

if(first) res = memberForPlace(i.first, context);

2620

else op(res, e->constraint(context));

2621

first = false;

2622

}

2623

return res;

2623

return res;

2624

}

2625

2626

Member PlusExpr::constraint(SimplificationContext& context) const {

2627

return commutativeCons(0, context, [](auto& a , auto b){ a += b;});

2628

}

2629

2630

Member SubtractExpr::constraint(SimplificationContext& context) const {

2631

Member res = _exprs[0]->constraint(context);

2632

for(size_t i = 1; i < _exprs.size(); ++i) res -= _exprs[i]->constraint(context);

2633

return res;

2634

}

2635

2636

Member MultiplyExpr::constraint(SimplificationContext& context) const {

2637

return commutativeCons(1, context, [](auto& a , auto b){ a *= b;});

2638

}

2639

2640

Member MinusExpr::constraint(SimplificationContext& context) const {

2641

Member neg(-1);

2642

return _expr->constraint(context) *= neg;

2643

}

2644

2645

Retval simplifyEX(Retval& r, SimplificationContext& context) {

2646

if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {

2647

return Retval(std::make_shared<NotCondition>(

2652

return Retval(std::make_shared<EXCondition>(r.formula));

2653

}

2654

}

2655

2656

Retval simplifyAX(Retval& r, SimplificationContext& context) {

2657

if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){

2658

return Retval(BooleanCondition::TRUE_CONSTANT);

2672

return Retval(std::make_shared<EFCondition>(r.formula));

2673

}

2674

}

2675

2676

Retval simplifyAF(Retval& r, SimplificationContext& context){

2677

if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){

2678

return Retval(BooleanCondition::TRUE_CONSTANT);

2682

return Retval(std::make_shared<AFCondition>(r.formula));

2683

}

2684

}

2685

2686

Retval simplifyEG(Retval& r, SimplificationContext& context){

2687

if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){

2688

return Retval(BooleanCondition::TRUE_CONSTANT);

2692

return Retval(std::make_shared<EGCondition>(r.formula));

2693

}

2694

}

2695

2696

Retval simplifyAG(Retval& r, SimplificationContext& context){

2697

if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){

2698

return Retval(BooleanCondition::TRUE_CONSTANT);

2720

Retval r = _cond->simplify(context);

2721

return context.negated() ? simplifyAX(r, context) : simplifyEX(r, context);

2722

}

2723

2724

Retval AXCondition::simplify(SimplificationContext& context) const {

2725

Retval r = _cond->simplify(context);

2726

return context.negated() ? simplifyEX(r, context) : simplifyAX(r, context);

2727

}

2728

2727

}

2728

2729

Retval EFCondition::simplify(SimplificationContext& context) const {

2730

Retval r = _cond->simplify(context);

2731

return context.negated() ? simplifyAG(r, context) : simplifyEF(r, context);

2731

return context.negated() ? simplifyAG(r, context) : simplifyEF(r, context);

2732

}

2733

2734

Retval AFCondition::simplify(SimplificationContext& context) const {

2735

Retval r = _cond->simplify(context);

2736

return context.negated() ? simplifyEG(r, context) : simplifyAF(r, context);

2736

return context.negated() ? simplifyEG(r, context) : simplifyAF(r, context);

2737

}

2738

2739

Retval EGCondition::simplify(SimplificationContext& context) const {

2740

Retval r = _cond->simplify(context);

2741

return context.negated() ? simplifyAF(r, context) : simplifyEG(r, context);

2741

return context.negated() ? simplifyAF(r, context) : simplifyEG(r, context);

2742

}

2743

2744

Retval AGCondition::simplify(SimplificationContext& context) const {

2745

Retval r = _cond->simplify(context);

2746

return context.negated() ? simplifyEF(r, context) : simplifyAG(r, context);

2746

return context.negated() ? simplifyEF(r, context) : simplifyAG(r, context);

2747

}

2748

2749

Retval EUCondition::simplify(SimplificationContext& context) const {

2750

// cannot push negation any further

2751

bool neg = context.negated();

2754

if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))

2755

{

2756

context.setNegate(neg);

2757

return neg ?

2757

return neg ?

2758

Retval(BooleanCondition::FALSE_CONSTANT) :

2759

Retval(BooleanCondition::TRUE_CONSTANT);

2760

}

2761

else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))

2762

{

2763

context.setNegate(neg);

2764

return neg ?

2764

return neg ?

2765

Retval(BooleanCondition::TRUE_CONSTANT) :

2766

Retval(BooleanCondition::FALSE_CONSTANT);

2766

Retval(BooleanCondition::FALSE_CONSTANT);

2767

}

2768

Retval r1 = _cond1->simplify(context);

2769

context.setNegate(neg);

2770

2771

if(context.negated()){

2772

if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){

2773

return Retval(std::make_shared<NotCondition>(

2788

}

2789

}

2790

}

2791

2792

Retval AUCondition::simplify(SimplificationContext& context) const {

2793

// cannot push negation any further

2794

bool neg = context.negated();

2797

if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))

2798

{

2799

context.setNegate(neg);

2800

return neg ?

2800

return neg ?

2801

Retval(BooleanCondition::FALSE_CONSTANT) :

2802

Retval(BooleanCondition::TRUE_CONSTANT);

2803

}

2804

else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))

2805

{

2806

context.setNegate(neg);

2807

return neg ?

2807

return neg ?

2808

Retval(BooleanCondition::TRUE_CONSTANT) :

2809

Retval(BooleanCondition::FALSE_CONSTANT);

2810

}

2811

Retval r1 = _cond1->simplify(context);

2812

context.setNegate(neg);

2813

2814

if(context.negated()){

2815

if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){

2816

return Retval(std::make_shared<NotCondition>(

2919

}

2920

return lps[0];

2921

}

2922

2923

Retval LogicalCondition::simplifyAnd(SimplificationContext& context) const {

2924

2925

std::vector<Condition_ptr> conditions;

2936

{

2937

continue;

2938

}

2939

2940

conditions.push_back(r.formula);

2941

lpsv.emplace_back(r.lps);

2942

neglps.emplace_back(r.neglps);

2943

}

2944

2945

if(conditions.size() == 0)

2946

{

2947

return Retval(BooleanCondition::TRUE_CONSTANT);

2953

if(!context.timeout() && !lps->satisfiable(context))

2954

{

2955

return Retval(BooleanCondition::FALSE_CONSTANT);

2956

}

2956

}

2957

}

2958

catch(std::bad_alloc& e)

2959

{

2960

// we are out of memory, deal with it.

2961

std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;

2962

}

2963

2964

// Lets try to see if the r1 AND r2 can ever be false at the same time

2965

// If not, then we know that r1 || r2 must be true.

2966

// we check this by checking if !r1 && !r2 is unsat

2967

2968

return Retval(

2969

makeAnd(conditions),

2969

makeAnd(conditions),

2970

std::move(lps),

2971

std::make_shared<UnionCollection>(std::move(neglps)));

2972

}

2973

2974

Retval LogicalCondition::simplifyOr(SimplificationContext& context) const {

2975

2976

std::vector<Condition_ptr> conditions;

2993

lps.push_back(r.lps);

2994

neglpsv.emplace_back(r.neglps);

2995

}

2996

2997

AbstractProgramCollection_ptr neglps = mergeLps(std::move(neglpsv));

2998

2999

if(conditions.size() == 0)

3005

if(!context.timeout() && !neglps->satisfiable(context))

3006

{

3007

return Retval(BooleanCondition::TRUE_CONSTANT);

3008

}

3008

}

3009

}

3010

catch(std::bad_alloc& e)

3011

{

3016

// Lets try to see if the r1 AND r2 can ever be false at the same time

3017

// If not, then we know that r1 || r2 must be true.

3018

// we check this by checking if !r1 && !r2 is unsat

3019

3020

return Retval(

3021

makeOr(conditions),

3022

std::make_shared<UnionCollection>(std::move(lps)),

3023

std::move(neglps));

3021

makeOr(conditions),

3022

std::make_shared<UnionCollection>(std::move(lps)),

3023

std::move(neglps));

3024

}

3025

3026

Retval AndCondition::simplify(SimplificationContext& context) const {

3027

if(context.timeout())

3028

{

3029

if(context.negated())

3029

if(context.negated())

3030

return Retval(std::make_shared<NotCondition>(

3031

makeAnd(_conds)));

3032

else

3032

else

3033

return Retval(

3034

makeAnd(_conds));

3035

}

3038

return simplifyOr(context);

3039

else

3040

return simplifyAnd(context);

3041

3042

}

3043

3044

Retval OrCondition::simplify(SimplificationContext& context) const {

3043

3044

Retval OrCondition::simplify(SimplificationContext& context) const {

3045

if(context.timeout())

3046

{

3047

if(context.negated())

3047

if(context.negated())

3048

return Retval(std::make_shared<NotCondition>(

3049

makeOr(_conds)));

3050

else

3050

else

3051

return Retval(makeOr(_conds));

3052

}

3053

if(context.negated())

3055

else

3056

return simplifyOr(context);

3057

}

3058

3059

Retval CompareConjunction::simplify(SimplificationContext& context) const {

3060

if(context.timeout())

3061

{

3064

std::vector<AbstractProgramCollection_ptr> neglps, lpsv;

3065

auto neg = context.negated() != _negated;

3066

std::vector<cons_t> nconstraints;

3067

for(auto& c : _constraints)

3067

for(auto& c : _constraints)

3068

{

3069

nconstraints.push_back(c);

3070

if(c._lower != 0 /*&& !context.timeout()*/ )

3088

neglps.push_back(nlp);

3089

}

3090

}

3091

3092

if(c._upper != std::numeric_limits<uint32_t>::max() /*&& !context.timeout()*/)

3093

{

3094

auto m1 = memberForPlace(c._place, context);

3110

neglps.push_back(nlp);

3111

}

3112

}

3113

3114

assert(nconstraints.size() > 0);

3115

if(nconstraints.back()._lower == 0 && nconstraints.back()._upper == std::numeric_limits<uint32_t>::max())

3116

nconstraints.pop_back();

3117

3118

assert(nconstraints.size() <= neglps.size()*2);

3119

}

3120

3121

auto lps = mergeLps(std::move(lpsv));

3122

3123

if(lps == nullptr && !context.timeout())

3122

3123

if(lps == nullptr && !context.timeout())

3124

{

3125

return Retval(BooleanCondition::getShared(!neg));

3126

}

3127

3128

try {

3129

if(!context.timeout() && lps && !lps->satisfiable(context))

3130

{

3131

return Retval(BooleanCondition::getShared(neg));

3132

}

3132

}

3133

}

3134

catch(std::bad_alloc& e)

3135

{

3142

try {

3143

// remove trivial rules from neglp

3144

int ncnt = neglps.size() - 1;

3145

for(int i = nconstraints.size() - 1; i >= 0; --i)

3145

for(int i = nconstraints.size() - 1; i >= 0; --i)

3146

{

3147

if(context.timeout()) break;

3148

assert(ncnt >= 0);

3161

c._upper = std::numeric_limits<uint32_t>::max();

3162

neglps.erase(neglps.begin() + ncnt);

3163

}

3164

if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)

3164

if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)

3165

nconstraints.erase(nconstraints.begin() + i);

3166

--ncnt;

3167

}

3171

{

3172

// we are out of memory, deal with it.

3173

std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;

3174

}

3174

}

3175

if(nconstraints.size() == 0)

3176

{

3177

return Retval(BooleanCondition::getShared(!neg));

3177

return Retval(BooleanCondition::getShared(!neg));

3178

}

3179

3180

3181

Condition_ptr rc = [&]() -> Condition_ptr {

3182

if(nconstraints.size() == 1)

3183

{

3209

else

3210

{

3211

if(neg) return std::make_shared<LessThanCondition>(lu, id);

3212

else return std::make_shared<LessThanOrEqualCondition>(id, lu);

3212

else return std::make_shared<LessThanOrEqualCondition>(id, lu);

3213

}

3214

}

3215

}

3218

return std::make_shared<CompareConjunction>(std::move(nconstraints), context.negated() != _negated);

3219

}

3220

}();

3221

3222

3223

if(!neg)

3224

{

3225

return Retval(

3226

rc,

3226

rc,

3227

std::move(lps),

3228

std::make_shared<UnionCollection>(std::move(neglps)));

3229

}

3230

else

3231

{

3232

return Retval(

3233

rc,

3233

rc,

3234

std::make_shared<UnionCollection>(std::move(neglps)),

3235

std::move(lps));

3235

std::move(lps));

3236

}

3237

}

3238

3239

Retval EqualCondition::simplify(SimplificationContext& context) const {

3240

3241

Member m1 = _expr1->constraint(context);

3242

Member m2 = _expr2->constraint(context);

3243

std::shared_ptr<AbstractProgramCollection> lps, neglps;

3249

int constant = m2.constant() - m1.constant();

3250

m1 -= m2;

3251

m2 = m1;

3252

neglps =

3252

neglps =

3253

std::make_shared<UnionCollection>(

3254

std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_GT),

3255

std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_LT));

3256

Member m3 = m2;

3257

lps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ);

3258

3259

if(context.negated()) lps.swap(neglps);

3260

}

3261

} else {

3262

lps = std::make_shared<SingleProgram>();

3263

neglps = std::make_shared<SingleProgram>();

3264

}

3265

3266

if (!context.timeout() && !lps->satisfiable(context)) {

3267

return Retval(BooleanCondition::FALSE_CONSTANT);

3268

}

3268

}

3269

else if(!context.timeout() && !neglps->satisfiable(context))

3270

{

3271

return Retval(BooleanCondition::TRUE_CONSTANT);

3272

}

3271

return Retval(BooleanCondition::TRUE_CONSTANT);

3272

}

3273

else {

3274

if (context.negated()) {

3275

return Retval(std::make_shared<NotEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));

3278

}

3279

}

3280

}

3281

3282

Retval NotEqualCondition::simplify(SimplificationContext& context) const {

3283

Member m1 = _expr1->constraint(context);

3284

Member m2 = _expr2->constraint(context);

3287

if ((m1.isZero() && m2.isZero()) || m1.substrationIsZero(m2)) {

3288

return Retval(std::make_shared<BooleanCondition>(

3289

context.negated() ? (m1.constant() == m2.constant()) : (m1.constant() != m2.constant())));

3290

} else{

3290

} else{

3291

int constant = m2.constant() - m1.constant();

3292

m1 -= m2;

3293

m2 = m1;

3294

lps =

3294

lps =

3295

std::make_shared<UnionCollection>(

3296

std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_GT),

3297

std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_LT));

3298

Member m3 = m2;

3299

neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ);

3300

3299

neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ);

3300

3301

if(context.negated()) lps.swap(neglps);

3302

}

3303

} else {

3306

}

3307

if (!context.timeout() && !lps->satisfiable(context)) {

3308

return Retval(BooleanCondition::FALSE_CONSTANT);

3309

}

3309

}

3310

else if(!context.timeout() && !neglps->satisfiable(context))

3311

{

3312

return Retval(BooleanCondition::TRUE_CONSTANT);

3312

return Retval(BooleanCondition::TRUE_CONSTANT);

3313

}

3314

else {

3315

if (context.negated()) {

3316

return Retval(std::make_shared<EqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));

3317

} else {

3318

return Retval(std::make_shared<NotEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));

3319

}

3319

}

3320

}

3321

}

3322

3323

Retval LessThanCondition::simplify(SimplificationContext& context) const {

3324

Member m1 = _expr1->constraint(context);

3325

Member m2 = _expr2->constraint(context);

3340

lps = std::make_shared<SingleProgram>();

3341

neglps = std::make_shared<SingleProgram>();

3342

}

3343

3344

if (!context.timeout() && !lps->satisfiable(context)) {

3345

return Retval(BooleanCondition::FALSE_CONSTANT);

3346

}

3347

else if(!context.timeout() && !neglps->satisfiable(context))

3348

{

3349

return Retval(BooleanCondition::TRUE_CONSTANT);

3349

return Retval(BooleanCondition::TRUE_CONSTANT);

3350

}

3351

else {

3352

if (context.negated()) {

3353

return Retval(std::make_shared<LessThanOrEqualCondition>(_expr2, _expr1), std::move(lps), std::move(neglps));

3354

} else {

3355

return Retval(std::make_shared<LessThanCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));

3356

}

3356

}

3357

}

3358

}

3359

3358

}

3359

3360

Retval LessThanOrEqualCondition::simplify(SimplificationContext& context) const {

3361

Member m1 = _expr1->constraint(context);

3362

Member m2 = _expr2->constraint(context);

3363

3364

AbstractProgramCollection_ptr lps, neglps;

3365

if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {

3366

// test for trivial comparison

3378

lps = std::make_shared<SingleProgram>();

3379

neglps = std::make_shared<SingleProgram>();

3380

}

3381

3382

assert(lps);

3383

assert(neglps);

3384

3390

if (context.negated()) {

3391

return Retval(std::make_shared<LessThanCondition>(_expr2, _expr1), std::move(lps), std::move(neglps));

3392

} else {

3393

return Retval(std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2),

3393

return Retval(std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2),

3394

std::move(lps), std::move(neglps));

3395

}

3395

}

3396

}

3397

}

3398

3399

Retval NotCondition::simplify(SimplificationContext& context) const {

3400

context.negate();

3401

Retval r = _cond->simplify(context);

3402

context.negate();

3403

return r;

3404

}

3405

3406

Retval BooleanCondition::simplify(SimplificationContext& context) const {

3407

if (context.negated()) {

3408

return Retval(getShared(!value));

3410

return Retval(getShared(value));

3411

}

3412

}

3413

3414

Retval DeadlockCondition::simplify(SimplificationContext& context) const {

3415

if (context.negated()) {

3416

return Retval(std::make_shared<NotCondition>(DeadlockCondition::DEADLOCK));

3418

return Retval(DeadlockCondition::DEADLOCK);

3419

}

3420

}

3421

3422

Retval UnfoldedUpperBoundsCondition::simplify(SimplificationContext& context) const

3421

3422

Retval UnfoldedUpperBoundsCondition::simplify(SimplificationContext& context) const

3423

{

3424

std::vector<place_t> next;

3425

std::vector<uint32_t> places;

3442

}

3443

return Retval(std::make_shared<UnfoldedUpperBoundsCondition>(next, bounds[nplaces].first-offset, offset));

3444

}

3445

3446

/******************** Check if query is a reachability query ********************/

3447

3448

bool EXCondition::isReachability(uint32_t depth) const {

3449

return false;

3450

}

3451

3452

bool EGCondition::isReachability(uint32_t depth) const {

3453

return false;

3454

}

3455

3456

bool EFCondition::isReachability(uint32_t depth) const {

3457

return depth > 0 ? false : _cond->isReachability(depth + 1);

3458

}

3459

3460

bool AXCondition::isReachability(uint32_t depth) const {

3461

return false;

3462

}

3463

3464

bool AGCondition::isReachability(uint32_t depth) const {

3465

return depth > 0 ? false : _cond->isReachability(depth + 1);

3466

}

3467

3468

bool AFCondition::isReachability(uint32_t depth) const {

3469

return false;

3470

}

3473

if (depth != 0) {

3474

return false;

3475

}

3476

3477

if (auto cond = dynamic_cast<FCondition*>(_cond.get())) {

3476

else if (auto cond = dynamic_cast<FCondition*>(_cond.get())) {

3478

3477

// EF is a reachability formula so skip checking the F.

3479

3478

return (*cond)[0]->isReachability(depth + 1);

3480

3479

}

3481

return _cond->isReachability(depth + 1);

3480

else return false;

3482

3481

}

3483

3482

3484

3483

bool ACondition::isReachability(uint32_t depth) const {

3485

3484

if (depth != 0) {

3486

3485

return false;

3487

3486

}

3488

if (auto cond = dynamic_cast<GCondition*>(_cond.get())) {

3487

else if (auto cond = dynamic_cast<GCondition*>(_cond.get())) {

3489

3488

return (*cond)[0]->isReachability(depth + 1);

3490

3489

}

3491

return _cond->isReachability(depth + 1);

3490

else return false;

3492

3491

}

3493

3492

3494

3493

bool UntilCondition::isReachability(uint32_t depth) const {

3495

3494

return false;

3496

3495

}

3497

3496

3498

3497

bool LogicalCondition::isReachability(uint32_t depth) const {

3499

3498

if(depth == 0) return false;

3500

3499

bool reachability = true;

3505

3504

}

3506

3505

return reachability;

3507

3506

}

3508

3507

3509

3508

bool CompareCondition::isReachability(uint32_t depth) const {

3510

3509

return depth > 0;

3511

3510

}

3512

3511

3513

3512

bool NotCondition::isReachability(uint32_t depth) const {

3514

3513

return _cond->isReachability(depth);

3515

3514

}

3516

3515

3517

3516

bool BooleanCondition::isReachability(uint32_t depth) const {

3518

3517

return depth > 0;

3519

3518

}

3520

3519

3521

3520

bool DeadlockCondition::isReachability(uint32_t depth) const {

3522

3521

return depth > 0;

3523

3522

}

3524

3523

3525

3524

bool UnfoldedUpperBoundsCondition::isReachability(uint32_t depth) const {

3526

3525

return depth > 0;

3527

3526

}

3528

3527

3529

3528

/******************** Prepare Reachability Queries ********************/

3530

3529

3531

3530

Condition_ptr EXCondition::prepareForReachability(bool negated) const {

3532

3531

return nullptr;

3533

3532

}

3534

3533

3535

3534

Condition_ptr EGCondition::prepareForReachability(bool negated) const {

3536

3535

return nullptr;

3537

3536

}

3538

3537

3539

3538

Condition_ptr EFCondition::prepareForReachability(bool negated) const {

3540

3539

_cond->setInvariant(negated);

3541

3540

return _cond;

3542

3541

}

3543

3542

3544

3543

Condition_ptr AXCondition::prepareForReachability(bool negated) const {

3545

3544

return nullptr;

3546

3545

}

3547

3546

3548

3547

Condition_ptr AGCondition::prepareForReachability(bool negated) const {

3549

3548

Condition_ptr cond = std::make_shared<NotCondition>(_cond);

3550

3549

cond->setInvariant(!negated);

3551

3550

return cond;

3552

3551

}

3553

3552

3554

3553

Condition_ptr AFCondition::prepareForReachability(bool negated) const {

3555

3554

return nullptr;

3556

3555

}

3557

3556

3558

3557

Condition_ptr ACondition::prepareForReachability(bool negated) const {

3559

3558

auto g = std::dynamic_pointer_cast<GCondition>(_cond);

3560

if (g) {

3561

return AGCondition((*g)[0]).prepareForReachability(negated);

3562

}

3563

else {

3564

// ugly hacking for `A true`.

3565

auto bcond = std::dynamic_pointer_cast<BooleanCondition>(_cond);

3566

if (bcond) {

3567

return bcond;

3568

}

3569

else return nullptr;

3570

}

3559

return g ? AGCondition((*g)[0]).prepareForReachability(negated) : nullptr;

3571

3560

}

3572

3561

3573

3562

Condition_ptr ECondition::prepareForReachability(bool negated) const {

3578

3567

Condition_ptr UntilCondition::prepareForReachability(bool negated) const {

3579

3568

return nullptr;

3580

3569

}

3581

3570

3582

3571

Condition_ptr LogicalCondition::prepareForReachability(bool negated) const {

3583

3572

return nullptr;

3584

3573

}

3586

3575

Condition_ptr CompareConjunction::prepareForReachability(bool negated) const {

3587

3576

return nullptr;

3588

3577

}

3589

3578

3590

3579

Condition_ptr CompareCondition::prepareForReachability(bool negated) const {

3591

3580

return nullptr;

3592

3581

}

3593

3582

3594

3583

Condition_ptr NotCondition::prepareForReachability(bool negated) const {

3595

3584

return _cond->prepareForReachability(!negated);

3596

3585

}

3597

3586

3598

3587

Condition_ptr BooleanCondition::prepareForReachability(bool negated) const {

3599

3588

return nullptr;

3600

3589

}

3601

3590

3602

3591

Condition_ptr DeadlockCondition::prepareForReachability(bool negated) const {

3603

3592

return nullptr;

3604

3593

}

3606

3595

Condition_ptr UnfoldedUpperBoundsCondition::prepareForReachability(bool negated) const {

3607

3596

return nullptr;

3608

3597

}

3609

3598

3610

3599

/******************** Prepare CTL Queries ********************/

3611

3600

3612

3601

Condition_ptr EGCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

3613

3602

++stats[0];

3614

3603

return AFCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);

3618

3607

++stats[1];

3619

3608

return EFCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);

3620

3609

}

3621

3610

3622

3611

Condition_ptr EXCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

3623

3612

return initialMarkingRW([&]() -> Condition_ptr {

3624

3613

auto a = _cond->pushNegation(stats, context, true, negated, initrw);

3629

3618

}

3630

3619

else

3631

3620

{

3632

if(a == BooleanCondition::FALSE_CONSTANT)

3621

if(a == BooleanCondition::FALSE_CONSTANT)

3633

3622

{ ++stats[3]; return a;}

3634

if(a == BooleanCondition::TRUE_CONSTANT)

3623

if(a == BooleanCondition::TRUE_CONSTANT)

3635

3624

{ ++stats[4]; return std::make_shared<NotCondition>(DeadlockCondition::DEADLOCK); }

3636

3625

a = std::make_shared<EXCondition>(a);

3637

3626

}

3649

3638

}

3650

3639

else

3651

3640

{

3652

if(a == BooleanCondition::TRUE_CONSTANT)

3641

if(a == BooleanCondition::TRUE_CONSTANT)

3653

3642

{ ++stats[6]; return a;}

3654

3643

if(a == BooleanCondition::FALSE_CONSTANT)

3655

3644

{ ++stats[7]; return DeadlockCondition::DEADLOCK; }

3659

3648

}, stats, context, nested, negated, initrw);

3660

3649

}

3661

3650

3662

3651

3663

3652

Condition_ptr EFCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

3664

3653

return initialMarkingRW([&]() -> Condition_ptr {

3665

3654

auto a = _cond->pushNegation(stats, context, true, false, initrw);

3670

3659

{

3671

3660

++stats[8];

3672

3661

return a->pushNegation(stats, context, nested, negated, initrw);

3673

}

3662

}

3674

3663

}

3675

3664

3676

3665

if(!a->isTemporal())

3679

3668

if(negated) return std::make_shared<NotCondition>(res);

3680

3669

return res;

3681

3670

}

3682

3671

3683

3672

if( dynamic_cast<EFCondition*>(a.get()))

3684

3673

{

3685

3674

++stats[9];

3714

3703

}

3715

3704

++stats[13];

3716

3705

std::vector<Condition_ptr> pef, atomic;

3717

for(auto& i : *cond)

3706

for(auto& i : *cond)

3718

3707

{

3719

3708

pef.push_back(std::make_shared<EFCondition>(i));

3720

3709

}

3722

3711

return a;

3723

3712

}

3724

3713

else

3725

{

3714

{

3726

3715

Condition_ptr b = std::make_shared<EFCondition>(a);

3727

3716

if(negated) b = std::make_shared<NotCondition>(b);

3728

3717

return b;

3740

3729

{

3741

3730

++stats[14];

3742

3731

return a->pushNegation(stats, context, nested, negated, initrw);

3743

}

3732

}

3744

3733

}

3745

3734

3746

3735

if(dynamic_cast<AFCondition*>(a.get()))

3747

3736

{

3748

3737

++stats[15];

3814

3803

return AFCondition(b).pushNegation(stats, context, nested, negated, initrw);

3815

3804

}

3816

3805

}

3817

3806

3818

3807

if(auto cond = dynamic_cast<AFCondition*>(b.get()))

3819

3808

{

3820

3809

++stats[22];

3855

3844

return makeOr(pef)->pushNegation(stats, context, nested, negated, initrw);

3856

3845

}

3857

3846

}

3858

3847

3859

3848

auto c = std::make_shared<AUCondition>(a, b);

3860

3849

if(negated) return std::make_shared<NotCondition>(c);

3861

3850

return c;

3889

3878

return EFCondition(b).pushNegation(stats, context, nested, negated, initrw);

3890

3879

}

3891

3880

}

3892

3881

3893

3882

if(dynamic_cast<EFCondition*>(b.get()))

3894

3883

{

3895

3884

++stats[28];

4026

4015

/*Boolean connectives */

4027

4016

Condition_ptr pushAnd(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)

4028

4017

{

4029

std::vector<Condition_ptr> nef, other;

4018

std::vector<Condition_ptr> nef, other;

4030

4019

for(auto& c : _conds)

4031

4020

{

4032

4021

auto n = c->pushNegation(stats, context, nested, negate_children, initrw);

4047

4036

{

4048

4037

other.emplace_back(n);

4049

4038

}

4050

}

4039

}

4051

4040

if(nef.size() + other.size() == 0)

4052

4041

return BooleanCondition::TRUE_CONSTANT;

4053

if(nef.size() + other.size() == 1)

4054

{

4055

return nef.size() == 0 ?

4056

other[0] :

4042

if(nef.size() + other.size() == 1)

4043

{

4044

return nef.size() == 0 ?

4045

other[0] :

4057

4046

std::make_shared<NotCondition>(std::make_shared<EFCondition>(nef[0]));

4058

4047

}

4059

4048

if(nef.size() != 0) other.push_back(

4060

4049

std::make_shared<NotCondition>(

4061

4050

std::make_shared<EFCondition>(

4062

makeOr(nef))));

4051

makeOr(nef))));

4063

4052

if(other.size() == 1) return other[0];

4064

4053

auto res = makeAnd(other);

4065

4054

return res;

4066

4055

}

4067

4056

4068

4057

Condition_ptr pushOr(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)

4069

4058

{

4070

std::vector<Condition_ptr> nef, other;

4059

std::vector<Condition_ptr> nef, other;

4071

4060

for(auto& c : _conds)

4072

4061

{

4073

4062

auto n = c->pushNegation(stats, context, nested, negate_children, initrw);

4090

4079

if(nef.size() + other.size() == 1) { return nef.size() == 0 ? other[0] : std::make_shared<EFCondition>(nef[0]);}

4091

4080

if(nef.size() != 0) other.push_back(

4092

4081

std::make_shared<EFCondition>(

4093

makeOr(nef)));

4082

makeOr(nef)));

4094

4083

if(other.size() == 1) return other[0];

4095

4084

return makeOr(other);

4096

4085

}

4102

4091

}, stats, context, nested, negated, initrw);

4103

4092

}

4104

4093

4105

4094

4106

4095

Condition_ptr AndCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4107

4096

return initialMarkingRW([&]() -> Condition_ptr {

4108

4097

return negated ? pushOr (_conds, stats, context, nested, true, initrw) :

4110

4099

4111

4100

}, stats, context, nested, negated, initrw);

4112

4101

}

4113

4102

4114

4103

Condition_ptr CompareConjunction::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4115

4104

return initialMarkingRW([&]() -> Condition_ptr {

4116

4105

return std::make_shared<CompareConjunction>(*this, negated);

4117

4106

}, stats, context, nested, negated, initrw);

4118

4107

}

4119

4108

4120

4109

4121

4110

Condition_ptr NotCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4122

4111

return initialMarkingRW([&]() -> Condition_ptr {

4123

4112

if(negated) ++stats[30];

4173

4162

if(auto p1 = std::dynamic_pointer_cast<PlusExpr>(_expr1))

4174

4163

if(auto p2 = std::dynamic_pointer_cast<PlusExpr>(_expr2))

4175

4164

remdup(p1, p2);

4176

4165

4177

4166

if(auto m1 = std::dynamic_pointer_cast<MultiplyExpr>(_expr1))

4178

4167

if(auto m2 = std::dynamic_pointer_cast<MultiplyExpr>(_expr2))

4179

remdup(m1, m2);

4180

4168

remdup(m1, m2);

4169

4181

4170

if(auto p1 = std::dynamic_pointer_cast<CommutativeExpr>(_expr1))

4182

4171

if(auto p2 = std::dynamic_pointer_cast<CommutativeExpr>(_expr2))

4183

4172

return p1->_exprs.size() + p1->_ids.size() + p2->_exprs.size() + p2->_ids.size() == 0;

4217

4206

if(negated == noteq) return std::make_shared<EqualCondition>((*org)[0], (*org)[1]);

4218

4207

else return std::make_shared<NotEqualCondition>((*org)[0], (*org)[1]);

4219

4208

}

4220

4209

4221

4210

Condition_ptr NotEqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4222

4211

return initialMarkingRW([&]() -> Condition_ptr {

4223

4212

return pushEqual(this, negated, true, context);

4224

4213

}, stats, context, nested, negated, initrw);

4225

4214

}

4226

4215

4227

4216

4228

4217

Condition_ptr EqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4229

4218

return initialMarkingRW([&]() -> Condition_ptr {

4230

4219

return pushEqual(this, negated, false, context);

4231

4220

}, stats, context, nested, negated, initrw);

4232

4221

}

4233

4222

4234

4223

Condition_ptr BooleanCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4235

4224

return initialMarkingRW([&]() -> Condition_ptr {

4236

4225

if(negated) return getShared(!value);

4237

4226

else return getShared(value);

4238

4227

}, stats, context, nested, negated, initrw);

4239

4228

}

4240

4229

4241

4230

Condition_ptr DeadlockCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4242

4231

return initialMarkingRW([&]() -> Condition_ptr {

4243

4232

if(negated) return std::make_shared<NotCondition>(DEADLOCK);

4244

4233

else return DEADLOCK;

4245

4234

}, stats, context, nested, negated, initrw);

4246

4235

}

4247

4236

4248

4237

Condition_ptr UnfoldedUpperBoundsCondition::pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) {

4249

4238

if(negated)

4250

4239

{

4260

4249

void postMerge(std::vector<Condition_ptr>& conds) {

4261

4250

std::sort(std::begin(conds), std::end(conds),

4262

4251

[](auto& a, auto& b) {

4263

return a->isTemporal() < b->isTemporal();

4252

return a->isTemporal() < b->isTemporal();

4264

4253

});

4265

}

4266

4254

}

4255

4267

4256

AndCondition::AndCondition(std::vector<Condition_ptr>&& conds) {

4268

4257

for (auto& c : conds) tryMerge<AndCondition>(_conds, c);

4269

4258

for (auto& c : _conds) _temporal = _temporal || c->isTemporal();

4270

4259

for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();

4271

4260

postMerge(_conds);

4272

4261

}

4273

4262

4274

4263

AndCondition::AndCondition(const std::vector<Condition_ptr>& conds) {

4275

4264

for (auto& c : conds) tryMerge<AndCondition>(_conds, c);

4276

4265

for (auto& c : _conds) _temporal = _temporal || c->isTemporal();

4277

4266

for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();

4278

4267

postMerge(_conds);

4279

4268

}

4280

4269

4281

4270

AndCondition::AndCondition(Condition_ptr left, Condition_ptr right) {

4282

4271

tryMerge<AndCondition>(_conds, left);

4283

4272

tryMerge<AndCondition>(_conds, right);

4285

4274

for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();

4286

4275

postMerge(_conds);

4287

4276

}

4288

4277

4289

4278

OrCondition::OrCondition(std::vector<Condition_ptr>&& conds) {

4290

4279

for (auto& c : conds) tryMerge<OrCondition>(_conds, c);

4291

4280

for (auto& c : _conds) _temporal = _temporal || c->isTemporal();

4292

4281

for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();

4293

4282

postMerge(_conds);

4294

4283

}

4295

4284

4296

4285

OrCondition::OrCondition(const std::vector<Condition_ptr>& conds) {

4297

4286

for (auto& c : conds) tryMerge<OrCondition>(_conds, c);

4298

4287

for (auto& c : _conds) _temporal = _temporal || c->isTemporal();

4299

4288

for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();

4300

4289

postMerge(_conds);

4301

4290

}

4302

4291

4303

4292

OrCondition::OrCondition(Condition_ptr left, Condition_ptr right) {

4304

4293

tryMerge<OrCondition>(_conds, left);

4305

4294

tryMerge<OrCondition>(_conds, right);

4307

4296

for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();

4308

4297

postMerge(_conds);

4309

4298

}

4310

4299

4311

4300

4312

4301

CompareConjunction::CompareConjunction(const std::vector<Condition_ptr>& conditions, bool negated)

4313

4302

{

4314

4303

_negated = negated;

4315

4304

merge(conditions, negated);

4316

4305

}

4317

4306

4318

4307

void CompareConjunction::merge(const CompareConjunction& other)

4319

4308

{

4320

4309

auto neg = _negated != other._negated;

4329

4318

{

4330

4319

if(neg)

4331

4320

c.invert();

4332

4321

4333

4322

if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)

4334

4323

{

4335

4324

continue;

4340

4329

assert(false);

4341

4330

exit(ErrorCode);

4342

4331

}

4343

4332

4344

4333

il = std::lower_bound(_constraints.begin(), _constraints.end(), c);

4345

4334

if(il == _constraints.end() || il->_place != c._place)

4346

4335

{

4353

4342

}

4354

4343

}

4355

4344

}

4356

4345

4357

4346

void CompareConjunction::merge(const std::vector<Condition_ptr>& conditions, bool negated)

4358

4347

{

4359

4348

for(auto& c : conditions)

4405

4394

}

4406

4395

if(negated)

4407

4396

next.invert();

4408

4397

4409

4398

auto lb = std::lower_bound(std::begin(_constraints), std::end(_constraints), next);

4410

4399

if(lb == std::end(_constraints) || lb->_place != next._place)

4411

4400

{

4412

4401

next._name = id->name();

4413

4402

_constraints.insert(lb, next);

4414

}

4403

}

4415

4404

else

4416

4405

{

4417

4406

assert(id->name().compare(lb->_name) == 0);

4418

4407

lb->intersect(next);

4419

4408

}

4420

}

4409

}

4421

4410

}

4422

4411

4423

4412

void CommutativeExpr::init(std::vector<Expr_ptr>&& exprs)

4424

4413

{

4425

4414

for (auto& e : exprs) {

4430

4419

}

4431

4420

else if (auto id = std::dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(e)) {

4432

4421

_ids.emplace_back(id->offset(), id->name());

4433

}

4422

}

4434

4423

else if(auto c = std::dynamic_pointer_cast<CommutativeExpr>(e))

4435

4424

{

4436

4425

// we should move up plus/multiply here when possible;

4440

4429

}

4441

4430

else

4442

4431

{

4443

_exprs.emplace_back(std::move(e));

4432

_exprs.emplace_back(std::move(e));

4444

4433

}

4445

4434

} else {

4446

4435

_exprs.emplace_back(std::move(e));

4447

4436

}

4448

4437

}

4449

4438

}

4450

4439

4451

4440

PlusExpr::PlusExpr(std::vector<Expr_ptr>&& exprs, bool tk) : CommutativeExpr(0), tk(tk)

4452

4441

{

4453

4442

init(std::move(exprs));

4454

4443

}

4455

4444

4456

4445

MultiplyExpr::MultiplyExpr(std::vector<Expr_ptr>&& exprs) : CommutativeExpr(1)

4457

4446

{

4458

4447

init(std::move(exprs));