From 102766e04c0a7f72422d2accca6eaf4ce6e7be29 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Thu, 11 May 2023 14:44:52 +0200
Subject: [PATCH] updated C++ MC-benchmarks
---
benchmarks/model_checking/C++/CAN_BUS_tlc.cpp | 253 ++++++++--
.../C++/Cruise_finite1_deterministic_MC.cpp | 463 ++++++++++++++++--
.../model_checking/C++/LandingGear_R6.cpp | 321 ++++++++++--
.../model_checking/C++/Lift_MC_Large.cpp | 32 +-
.../C++/Train1_Lukas_POR_v3.cpp | 158 +++++-
...rain_1_beebook_deterministic_MC_POR_v2.cpp | 159 +++++-
benchmarks/model_checking/C++/nota_v2.cpp | 353 +++++++++----
7 files changed, 1483 insertions(+), 256 deletions(-)
diff --git a/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp b/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp
index 69e4a0320..95ce7b51c 100644
--- a/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp
+++ b/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp
@@ -1020,11 +1020,11 @@ class CAN_BUS_tlc {
}
friend bool operator ==(const CAN_BUS_tlc& o1, const CAN_BUS_tlc& o2) {
- return o1._get_BUSpriority() == o2._get_BUSpriority() && o1._get_BUSvalue() == o2._get_BUSvalue() && o1._get_BUSwrite() == o2._get_BUSwrite() && o1._get_T1_state() == o2._get_T1_state() && o1._get_T1_timer() == o2._get_T1_timer() && o1._get_T1_writevalue() == o2._get_T1_writevalue() && o1._get_T2_mode() == o2._get_T2_mode() && o1._get_T2_readpriority() == o2._get_T2_readpriority() && o1._get_T2_readvalue() == o2._get_T2_readvalue() && o1._get_T2_state() == o2._get_T2_state() && o1._get_T2_timer() == o2._get_T2_timer() && o1._get_T2_writevalue() == o2._get_T2_writevalue() && o1._get_T2v() == o2._get_T2v() && o1._get_T3_enabled() == o2._get_T3_enabled() && o1._get_T3_evaluated() == o2._get_T3_evaluated() && o1._get_T3_readpriority() == o2._get_T3_readpriority() && o1._get_T3_readvalue() == o2._get_T3_readvalue() && o1._get_T3_state() == o2._get_T3_state();
+ return o1._get_NATSET() == o2._get_NATSET() && o1._get_BUSpriority() == o2._get_BUSpriority() && o1._get_BUSvalue() == o2._get_BUSvalue() && o1._get_BUSwrite() == o2._get_BUSwrite() && o1._get_T1_state() == o2._get_T1_state() && o1._get_T1_timer() == o2._get_T1_timer() && o1._get_T1_writevalue() == o2._get_T1_writevalue() && o1._get_T2_mode() == o2._get_T2_mode() && o1._get_T2_readpriority() == o2._get_T2_readpriority() && o1._get_T2_readvalue() == o2._get_T2_readvalue() && o1._get_T2_state() == o2._get_T2_state() && o1._get_T2_timer() == o2._get_T2_timer() && o1._get_T2_writevalue() == o2._get_T2_writevalue() && o1._get_T2v() == o2._get_T2v() && o1._get_T3_enabled() == o2._get_T3_enabled() && o1._get_T3_evaluated() == o2._get_T3_evaluated() && o1._get_T3_readpriority() == o2._get_T3_readpriority() && o1._get_T3_readvalue() == o2._get_T3_readvalue() && o1._get_T3_state() == o2._get_T3_state();
}
friend bool operator !=(const CAN_BUS_tlc& o1, const CAN_BUS_tlc& o2) {
- return o1._get_BUSpriority() != o2._get_BUSpriority() || o1._get_BUSvalue() != o2._get_BUSvalue() || o1._get_BUSwrite() != o2._get_BUSwrite() || o1._get_T1_state() != o2._get_T1_state() || o1._get_T1_timer() != o2._get_T1_timer() || o1._get_T1_writevalue() != o2._get_T1_writevalue() || o1._get_T2_mode() != o2._get_T2_mode() || o1._get_T2_readpriority() != o2._get_T2_readpriority() || o1._get_T2_readvalue() != o2._get_T2_readvalue() || o1._get_T2_state() != o2._get_T2_state() || o1._get_T2_timer() != o2._get_T2_timer() || o1._get_T2_writevalue() != o2._get_T2_writevalue() || o1._get_T2v() != o2._get_T2v() || o1._get_T3_enabled() != o2._get_T3_enabled() || o1._get_T3_evaluated() != o2._get_T3_evaluated() || o1._get_T3_readpriority() != o2._get_T3_readpriority() || o1._get_T3_readvalue() != o2._get_T3_readvalue() || o1._get_T3_state() != o2._get_T3_state();
+ return o1._get_NATSET() != o2._get_NATSET() || o1._get_BUSpriority() != o2._get_BUSpriority() || o1._get_BUSvalue() != o2._get_BUSvalue() || o1._get_BUSwrite() != o2._get_BUSwrite() || o1._get_T1_state() != o2._get_T1_state() || o1._get_T1_timer() != o2._get_T1_timer() || o1._get_T1_writevalue() != o2._get_T1_writevalue() || o1._get_T2_mode() != o2._get_T2_mode() || o1._get_T2_readpriority() != o2._get_T2_readpriority() || o1._get_T2_readvalue() != o2._get_T2_readvalue() || o1._get_T2_state() != o2._get_T2_state() || o1._get_T2_timer() != o2._get_T2_timer() || o1._get_T2_writevalue() != o2._get_T2_writevalue() || o1._get_T2v() != o2._get_T2v() || o1._get_T3_enabled() != o2._get_T3_enabled() || o1._get_T3_evaluated() != o2._get_T3_evaluated() || o1._get_T3_readpriority() != o2._get_T3_readpriority() || o1._get_T3_readvalue() != o2._get_T3_readvalue() || o1._get_T3_state() != o2._get_T3_state();
}
int hashCode() const {
@@ -1165,7 +1165,6 @@ class ModelChecker {
CAN_BUS_tlc state = next();
std::unordered_set<CAN_BUS_tlc, CAN_BUS_tlc::Hash, CAN_BUS_tlc::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
@@ -1218,7 +1217,6 @@ class ModelChecker {
CAN_BUS_tlc state = next();
std::packaged_task<void()> task([&, state] {
std::unordered_set<CAN_BUS_tlc, CAN_BUS_tlc::Hash, CAN_BUS_tlc::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
{
@@ -1351,7 +1349,7 @@ class ModelChecker {
return state;
}
}
- }
+ };
}
std::unordered_set<CAN_BUS_tlc, CAN_BUS_tlc::Hash, CAN_BUS_tlc::HashEqual> generateNextStates(const CAN_BUS_tlc& state) {
@@ -1361,6 +1359,7 @@ class ModelChecker {
copiedState.T1Evaluate();
copiedState.stateAccessedVia = "T1Evaluate";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BInteger> _trid_2 = state._tr_T1Calculate(isCaching);
for(const BInteger& param : _trid_2) {
@@ -1370,6 +1369,7 @@ class ModelChecker {
copiedState.T1Calculate(_tmp_1);
copiedState.stateAccessedVia = "T1Calculate";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BInteger, BInteger >> _trid_3 = state._tr_T1SendResult(isCaching);
for(const BTuple<BInteger, BInteger >& param : _trid_3) {
@@ -1380,6 +1380,7 @@ class ModelChecker {
copiedState.T1SendResult(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "T1SendResult";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BInteger> _trid_4 = state._tr_T1Wait(isCaching);
for(const BInteger& param : _trid_4) {
@@ -1389,12 +1390,14 @@ class ModelChecker {
copiedState.T1Wait(_tmp_1);
copiedState.stateAccessedVia = "T1Wait";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T2Evaluate(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T2Evaluate"]);
copiedState.T2Evaluate();
copiedState.stateAccessedVia = "T2Evaluate";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BInteger, BInteger >> _trid_6 = state._tr_T2ReadBus(isCaching);
for(const BTuple<BInteger, BInteger >& param : _trid_6) {
@@ -1405,18 +1408,21 @@ class ModelChecker {
copiedState.T2ReadBus(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "T2ReadBus";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T2Reset(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T2Reset"]);
copiedState.T2Reset();
copiedState.stateAccessedVia = "T2Reset";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T2Complete(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T2Complete"]);
copiedState.T2Complete();
copiedState.stateAccessedVia = "T2Complete";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BInteger> _trid_9 = state._tr_T2ReleaseBus(isCaching);
for(const BInteger& param : _trid_9) {
@@ -1426,12 +1432,14 @@ class ModelChecker {
copiedState.T2ReleaseBus(_tmp_1);
copiedState.stateAccessedVia = "T2ReleaseBus";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T2Calculate(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T2Calculate"]);
copiedState.T2Calculate();
copiedState.stateAccessedVia = "T2Calculate";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BInteger, BInteger >> _trid_11 = state._tr_T2WriteBus(isCaching);
for(const BTuple<BInteger, BInteger >& param : _trid_11) {
@@ -1442,6 +1450,7 @@ class ModelChecker {
copiedState.T2WriteBus(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "T2WriteBus";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BInteger> _trid_12 = state._tr_T2Wait(isCaching);
for(const BInteger& param : _trid_12) {
@@ -1451,18 +1460,21 @@ class ModelChecker {
copiedState.T2Wait(_tmp_1);
copiedState.stateAccessedVia = "T2Wait";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T3Initiate(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T3Initiate"]);
copiedState.T3Initiate();
copiedState.stateAccessedVia = "T3Initiate";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T3Evaluate(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T3Evaluate"]);
copiedState.T3Evaluate();
copiedState.stateAccessedVia = "T3Evaluate";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BInteger, BInteger >> _trid_15 = state._tr_T3writebus(isCaching);
for(const BTuple<BInteger, BInteger >& param : _trid_15) {
@@ -1473,6 +1485,7 @@ class ModelChecker {
copiedState.T3writebus(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "T3writebus";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BInteger, BInteger >> _trid_16 = state._tr_T3Read(isCaching);
for(const BTuple<BInteger, BInteger >& param : _trid_16) {
@@ -1483,12 +1496,14 @@ class ModelChecker {
copiedState.T3Read(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "T3Read";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T3Poll(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T3Poll"]);
copiedState.T3Poll();
copiedState.stateAccessedVia = "T3Poll";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BInteger> _trid_18 = state._tr_T3ReleaseBus(isCaching);
for(const BInteger& param : _trid_18) {
@@ -1498,18 +1513,21 @@ class ModelChecker {
copiedState.T3ReleaseBus(_tmp_1);
copiedState.stateAccessedVia = "T3ReleaseBus";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T3Wait(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T3Wait"]);
copiedState.T3Wait();
copiedState.stateAccessedVia = "T3Wait";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_T3ReEnableWait(isCaching)) {
CAN_BUS_tlc copiedState = state._copy(guardDependency["T3ReEnableWait"]);
copiedState.T3ReEnableWait();
copiedState.stateAccessedVia = "T3ReEnableWait";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BInteger> _trid_21 = state._tr_Update(isCaching);
for(const BInteger& param : _trid_21) {
@@ -1519,117 +1537,296 @@ class ModelChecker {
copiedState.Update(_tmp_1);
copiedState.stateAccessedVia = "Update";
result.insert(copiedState);
+ transitions += 1;
}
return result;
}
bool invariantViolated(const CAN_BUS_tlc& state) {
+ std::unordered_set<string> dependentInvariantsOfState;
+ if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
if(isCaching) {
- std::unordered_set<string> dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_1()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_2") == dependentInvariantsOfState.end()) {
if(!state._check_inv_2()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_2()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_3") == dependentInvariantsOfState.end()) {
if(!state._check_inv_3()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_3()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_4") == dependentInvariantsOfState.end()) {
if(!state._check_inv_4()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_4()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_5") == dependentInvariantsOfState.end()) {
if(!state._check_inv_5()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_5()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_6") == dependentInvariantsOfState.end()) {
if(!state._check_inv_6()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_6()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_7") == dependentInvariantsOfState.end()) {
if(!state._check_inv_7()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_7()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_8") == dependentInvariantsOfState.end()) {
if(!state._check_inv_8()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_8()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_9") == dependentInvariantsOfState.end()) {
if(!state._check_inv_9()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_9()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_10") == dependentInvariantsOfState.end()) {
if(!state._check_inv_10()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_10()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_11") == dependentInvariantsOfState.end()) {
if(!state._check_inv_11()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_11()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_12") == dependentInvariantsOfState.end()) {
if(!state._check_inv_12()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_12()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_13") == dependentInvariantsOfState.end()) {
if(!state._check_inv_13()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_13()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_14") == dependentInvariantsOfState.end()) {
if(!state._check_inv_14()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_14()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_15") == dependentInvariantsOfState.end()) {
if(!state._check_inv_15()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_15()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_16") == dependentInvariantsOfState.end()) {
if(!state._check_inv_16()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_16()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_17") == dependentInvariantsOfState.end()) {
if(!state._check_inv_17()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_17()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_18") == dependentInvariantsOfState.end()) {
if(!state._check_inv_18()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_18()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_19") == dependentInvariantsOfState.end()) {
if(!state._check_inv_19()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_19" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_19()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_19" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_20") == dependentInvariantsOfState.end()) {
if(!state._check_inv_20()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_20" << "\n";
+ return true;
}
}
- return false;
+ } else {
+ if(!state._check_inv_20()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_20" << "\n";
+ return true;
+ }
}
- return !(state._check_inv_1() && state._check_inv_2() && state._check_inv_3() && state._check_inv_4() && state._check_inv_5() && state._check_inv_6() && state._check_inv_7() && state._check_inv_8() && state._check_inv_9() && state._check_inv_10() && state._check_inv_11() && state._check_inv_12() && state._check_inv_13() && state._check_inv_14() && state._check_inv_15() && state._check_inv_16() && state._check_inv_17() && state._check_inv_18() && state._check_inv_19() && state._check_inv_20());
+
+ return false;
}
diff --git a/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp b/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp
index 02d0fd98d..a6f64d4c7 100644
--- a/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp
+++ b/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp
@@ -1148,7 +1148,6 @@ class ModelChecker {
Cruise_finite1_deterministic_MC state = next();
std::unordered_set<Cruise_finite1_deterministic_MC, Cruise_finite1_deterministic_MC::Hash, Cruise_finite1_deterministic_MC::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
@@ -1201,7 +1200,6 @@ class ModelChecker {
Cruise_finite1_deterministic_MC state = next();
std::packaged_task<void()> task([&, state] {
std::unordered_set<Cruise_finite1_deterministic_MC, Cruise_finite1_deterministic_MC::Hash, Cruise_finite1_deterministic_MC::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
{
@@ -1344,7 +1342,7 @@ class ModelChecker {
return state;
}
}
- }
+ };
}
std::unordered_set<Cruise_finite1_deterministic_MC, Cruise_finite1_deterministic_MC::Hash, Cruise_finite1_deterministic_MC::HashEqual> generateNextStates(const Cruise_finite1_deterministic_MC& state) {
@@ -1354,12 +1352,14 @@ class ModelChecker {
copiedState.CruiseBecomesNotAllowed();
copiedState.stateAccessedVia = "CruiseBecomesNotAllowed";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_CruiseBecomesAllowed(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["CruiseBecomesAllowed"]);
copiedState.CruiseBecomesAllowed();
copiedState.stateAccessedVia = "CruiseBecomesAllowed";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BBoolean, BBoolean >> _trid_3 = state._tr_SetCruiseSpeed(isCaching);
for(const BTuple<BBoolean, BBoolean >& param : _trid_3) {
@@ -1370,6 +1370,7 @@ class ModelChecker {
copiedState.SetCruiseSpeed(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "SetCruiseSpeed";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BBoolean, BBoolean >> _trid_4 = state._tr_CCInitialisationFinished(isCaching);
for(const BTuple<BBoolean, BBoolean >& param : _trid_4) {
@@ -1380,12 +1381,14 @@ class ModelChecker {
copiedState.CCInitialisationFinished(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "CCInitialisationFinished";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_CCInitialisationDelayFinished(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["CCInitialisationDelayFinished"]);
copiedState.CCInitialisationDelayFinished();
copiedState.stateAccessedVia = "CCInitialisationDelayFinished";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BBoolean, BBoolean >> _trid_6 = state._tr_CruiseSpeedChangeFinished(isCaching);
for(const BTuple<BBoolean, BBoolean >& param : _trid_6) {
@@ -1396,96 +1399,112 @@ class ModelChecker {
copiedState.CruiseSpeedChangeFinished(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "CruiseSpeedChangeFinished";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_CruiseSpeedChangeDelayFinished(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["CruiseSpeedChangeDelayFinished"]);
copiedState.CruiseSpeedChangeDelayFinished();
copiedState.stateAccessedVia = "CruiseSpeedChangeDelayFinished";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_CruiseOff(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["CruiseOff"]);
copiedState.CruiseOff();
copiedState.stateAccessedVia = "CruiseOff";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ExternalForcesBecomesExtreme(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ExternalForcesBecomesExtreme"]);
copiedState.ExternalForcesBecomesExtreme();
copiedState.stateAccessedVia = "ExternalForcesBecomesExtreme";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ExternalForcesBecomesNormal(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ExternalForcesBecomesNormal"]);
copiedState.ExternalForcesBecomesNormal();
copiedState.stateAccessedVia = "ExternalForcesBecomesNormal";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_VehicleLeavesCruiseSpeed(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["VehicleLeavesCruiseSpeed"]);
copiedState.VehicleLeavesCruiseSpeed();
copiedState.stateAccessedVia = "VehicleLeavesCruiseSpeed";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_VehicleReachesCruiseSpeed(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["VehicleReachesCruiseSpeed"]);
copiedState.VehicleReachesCruiseSpeed();
copiedState.stateAccessedVia = "VehicleReachesCruiseSpeed";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_VehicleExceedsMaxCruiseSpeed(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["VehicleExceedsMaxCruiseSpeed"]);
copiedState.VehicleExceedsMaxCruiseSpeed();
copiedState.stateAccessedVia = "VehicleExceedsMaxCruiseSpeed";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_VehicleFallsBelowMaxCruiseSpeed(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["VehicleFallsBelowMaxCruiseSpeed"]);
copiedState.VehicleFallsBelowMaxCruiseSpeed();
copiedState.stateAccessedVia = "VehicleFallsBelowMaxCruiseSpeed";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleDistanceBecomesVeryClose(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleDistanceBecomesVeryClose"]);
copiedState.ObstacleDistanceBecomesVeryClose();
copiedState.stateAccessedVia = "ObstacleDistanceBecomesVeryClose";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleDistanceBecomesClose(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleDistanceBecomesClose"]);
copiedState.ObstacleDistanceBecomesClose();
copiedState.stateAccessedVia = "ObstacleDistanceBecomesClose";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleDistanceBecomesBig(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleDistanceBecomesBig"]);
copiedState.ObstacleDistanceBecomesBig();
copiedState.stateAccessedVia = "ObstacleDistanceBecomesBig";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleStartsTravelFaster(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleStartsTravelFaster"]);
copiedState.ObstacleStartsTravelFaster();
copiedState.stateAccessedVia = "ObstacleStartsTravelFaster";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleStopsTravelFaster(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleStopsTravelFaster"]);
copiedState.ObstacleStopsTravelFaster();
copiedState.stateAccessedVia = "ObstacleStopsTravelFaster";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleStartsTravelSlower(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleStartsTravelSlower"]);
copiedState.ObstacleStartsTravelSlower();
copiedState.stateAccessedVia = "ObstacleStartsTravelSlower";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleStopsTravelSlower(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleStopsTravelSlower"]);
copiedState.ObstacleStopsTravelSlower();
copiedState.stateAccessedVia = "ObstacleStopsTravelSlower";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<Cruise_finite1_deterministic_MC::RSset, Cruise_finite1_deterministic_MC::ODset >> _trid_22 = state._tr_ObstacleAppearsWhenCruiseActive(isCaching);
for(const BTuple<Cruise_finite1_deterministic_MC::RSset, Cruise_finite1_deterministic_MC::ODset >& param : _trid_22) {
@@ -1496,6 +1515,7 @@ class ModelChecker {
copiedState.ObstacleAppearsWhenCruiseActive(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "ObstacleAppearsWhenCruiseActive";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Cruise_finite1_deterministic_MC::RSset> _trid_23 = state._tr_ObstacleAppearsWhenCruiseInactive(isCaching);
for(const Cruise_finite1_deterministic_MC::RSset& param : _trid_23) {
@@ -1505,12 +1525,14 @@ class ModelChecker {
copiedState.ObstacleAppearsWhenCruiseInactive(_tmp_1);
copiedState.stateAccessedVia = "ObstacleAppearsWhenCruiseInactive";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleDisappears(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleDisappears"]);
copiedState.ObstacleDisappears();
copiedState.stateAccessedVia = "ObstacleDisappears";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BBoolean, BBoolean >> _trid_25 = state._tr_VehicleManageObstacle(isCaching);
for(const BTuple<BBoolean, BBoolean >& param : _trid_25) {
@@ -1521,218 +1543,569 @@ class ModelChecker {
copiedState.VehicleManageObstacle(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "VehicleManageObstacle";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_ObstacleBecomesOld(isCaching)) {
Cruise_finite1_deterministic_MC copiedState = state._copy(guardDependency["ObstacleBecomesOld"]);
copiedState.ObstacleBecomesOld();
copiedState.stateAccessedVia = "ObstacleBecomesOld";
result.insert(copiedState);
+ transitions += 1;
}
return result;
}
bool invariantViolated(const Cruise_finite1_deterministic_MC& state) {
+ std::unordered_set<string> dependentInvariantsOfState;
+ if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
if(isCaching) {
- std::unordered_set<string> dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_1()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_2") == dependentInvariantsOfState.end()) {
if(!state._check_inv_2()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_2()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_3") == dependentInvariantsOfState.end()) {
if(!state._check_inv_3()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_3()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_4") == dependentInvariantsOfState.end()) {
if(!state._check_inv_4()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_4()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_5") == dependentInvariantsOfState.end()) {
if(!state._check_inv_5()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_5()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_6") == dependentInvariantsOfState.end()) {
if(!state._check_inv_6()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_6()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_7") == dependentInvariantsOfState.end()) {
if(!state._check_inv_7()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_7()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_8") == dependentInvariantsOfState.end()) {
if(!state._check_inv_8()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_8()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_9") == dependentInvariantsOfState.end()) {
if(!state._check_inv_9()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_9()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_10") == dependentInvariantsOfState.end()) {
if(!state._check_inv_10()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_10()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_11") == dependentInvariantsOfState.end()) {
if(!state._check_inv_11()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_11()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_12") == dependentInvariantsOfState.end()) {
if(!state._check_inv_12()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_12()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_13") == dependentInvariantsOfState.end()) {
if(!state._check_inv_13()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_13()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_14") == dependentInvariantsOfState.end()) {
if(!state._check_inv_14()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_14()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_15") == dependentInvariantsOfState.end()) {
if(!state._check_inv_15()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_15()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_16") == dependentInvariantsOfState.end()) {
if(!state._check_inv_16()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_16()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_17") == dependentInvariantsOfState.end()) {
if(!state._check_inv_17()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_17()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_18") == dependentInvariantsOfState.end()) {
if(!state._check_inv_18()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_18()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_19") == dependentInvariantsOfState.end()) {
if(!state._check_inv_19()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_19" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_19()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_19" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_20") == dependentInvariantsOfState.end()) {
if(!state._check_inv_20()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_20" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_20()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_20" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_21") == dependentInvariantsOfState.end()) {
if(!state._check_inv_21()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_21" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_21()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_21" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_22") == dependentInvariantsOfState.end()) {
if(!state._check_inv_22()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_22" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_22()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_22" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_23") == dependentInvariantsOfState.end()) {
if(!state._check_inv_23()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_23" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_23()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_23" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_24") == dependentInvariantsOfState.end()) {
if(!state._check_inv_24()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_24" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_24()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_24" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_25") == dependentInvariantsOfState.end()) {
if(!state._check_inv_25()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_25" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_25()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_25" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_26") == dependentInvariantsOfState.end()) {
if(!state._check_inv_26()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_26" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_26()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_26" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_27") == dependentInvariantsOfState.end()) {
if(!state._check_inv_27()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_27" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_27()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_27" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_28") == dependentInvariantsOfState.end()) {
if(!state._check_inv_28()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_28" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_28()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_28" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_29") == dependentInvariantsOfState.end()) {
if(!state._check_inv_29()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_29" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_29()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_29" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_30") == dependentInvariantsOfState.end()) {
if(!state._check_inv_30()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_30" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_30()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_30" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_31") == dependentInvariantsOfState.end()) {
if(!state._check_inv_31()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_31" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_31()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_31" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_32") == dependentInvariantsOfState.end()) {
if(!state._check_inv_32()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_32" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_32()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_32" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_33") == dependentInvariantsOfState.end()) {
if(!state._check_inv_33()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_33" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_33()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_33" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_34") == dependentInvariantsOfState.end()) {
if(!state._check_inv_34()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_34" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_34()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_34" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_35") == dependentInvariantsOfState.end()) {
if(!state._check_inv_35()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_35" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_35()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_35" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_36") == dependentInvariantsOfState.end()) {
if(!state._check_inv_36()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_36" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_36()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_36" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_37") == dependentInvariantsOfState.end()) {
if(!state._check_inv_37()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_37" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_37()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_37" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_38") == dependentInvariantsOfState.end()) {
if(!state._check_inv_38()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_38" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_38()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_38" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_39") == dependentInvariantsOfState.end()) {
if(!state._check_inv_39()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_39" << "\n";
+ return true;
}
}
- return false;
+ } else {
+ if(!state._check_inv_39()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_39" << "\n";
+ return true;
+ }
}
- return !(state._check_inv_1() && state._check_inv_2() && state._check_inv_3() && state._check_inv_4() && state._check_inv_5() && state._check_inv_6() && state._check_inv_7() && state._check_inv_8() && state._check_inv_9() && state._check_inv_10() && state._check_inv_11() && state._check_inv_12() && state._check_inv_13() && state._check_inv_14() && state._check_inv_15() && state._check_inv_16() && state._check_inv_17() && state._check_inv_18() && state._check_inv_19() && state._check_inv_20() && state._check_inv_21() && state._check_inv_22() && state._check_inv_23() && state._check_inv_24() && state._check_inv_25() && state._check_inv_26() && state._check_inv_27() && state._check_inv_28() && state._check_inv_29() && state._check_inv_30() && state._check_inv_31() && state._check_inv_32() && state._check_inv_33() && state._check_inv_34() && state._check_inv_35() && state._check_inv_36() && state._check_inv_37() && state._check_inv_38() && state._check_inv_39());
+
+ return false;
}
diff --git a/benchmarks/model_checking/C++/LandingGear_R6.cpp b/benchmarks/model_checking/C++/LandingGear_R6.cpp
index 1550b6d6b..feb1f0122 100644
--- a/benchmarks/model_checking/C++/LandingGear_R6.cpp
+++ b/benchmarks/model_checking/C++/LandingGear_R6.cpp
@@ -1570,7 +1570,6 @@ class ModelChecker {
LandingGear_R6 state = next();
std::unordered_set<LandingGear_R6, LandingGear_R6::Hash, LandingGear_R6::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
@@ -1623,7 +1622,6 @@ class ModelChecker {
LandingGear_R6 state = next();
std::packaged_task<void()> task([&, state] {
std::unordered_set<LandingGear_R6, LandingGear_R6::Hash, LandingGear_R6::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
{
@@ -1790,7 +1788,7 @@ class ModelChecker {
return state;
}
}
- }
+ };
}
std::unordered_set<LandingGear_R6, LandingGear_R6::Hash, LandingGear_R6::HashEqual> generateNextStates(const LandingGear_R6& state) {
@@ -1800,108 +1798,126 @@ class ModelChecker {
copiedState.begin_flying();
copiedState.stateAccessedVia = "begin_flying";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_land_plane(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["land_plane"]);
copiedState.land_plane();
copiedState.stateAccessedVia = "land_plane";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_open_valve_door_open(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["open_valve_door_open"]);
copiedState.open_valve_door_open();
copiedState.stateAccessedVia = "open_valve_door_open";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_close_valve_door_open(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["close_valve_door_open"]);
copiedState.close_valve_door_open();
copiedState.stateAccessedVia = "close_valve_door_open";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_open_valve_door_close(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["open_valve_door_close"]);
copiedState.open_valve_door_close();
copiedState.stateAccessedVia = "open_valve_door_close";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_close_valve_door_close(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["close_valve_door_close"]);
copiedState.close_valve_door_close();
copiedState.stateAccessedVia = "close_valve_door_close";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_open_valve_retract_gear(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["open_valve_retract_gear"]);
copiedState.open_valve_retract_gear();
copiedState.stateAccessedVia = "open_valve_retract_gear";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_close_valve_retract_gear(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["close_valve_retract_gear"]);
copiedState.close_valve_retract_gear();
copiedState.stateAccessedVia = "close_valve_retract_gear";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_open_valve_extend_gear(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["open_valve_extend_gear"]);
copiedState.open_valve_extend_gear();
copiedState.stateAccessedVia = "open_valve_extend_gear";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_close_valve_extend_gear(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["close_valve_extend_gear"]);
copiedState.close_valve_extend_gear();
copiedState.stateAccessedVia = "close_valve_extend_gear";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stimulate_open_door_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stimulate_open_door_valve"]);
copiedState.con_stimulate_open_door_valve();
copiedState.stateAccessedVia = "con_stimulate_open_door_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stop_stimulate_open_door_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stop_stimulate_open_door_valve"]);
copiedState.con_stop_stimulate_open_door_valve();
copiedState.stateAccessedVia = "con_stop_stimulate_open_door_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stimulate_close_door_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stimulate_close_door_valve"]);
copiedState.con_stimulate_close_door_valve();
copiedState.stateAccessedVia = "con_stimulate_close_door_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stop_stimulate_close_door_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stop_stimulate_close_door_valve"]);
copiedState.con_stop_stimulate_close_door_valve();
copiedState.stateAccessedVia = "con_stop_stimulate_close_door_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stimulate_retract_gear_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stimulate_retract_gear_valve"]);
copiedState.con_stimulate_retract_gear_valve();
copiedState.stateAccessedVia = "con_stimulate_retract_gear_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stop_stimulate_retract_gear_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stop_stimulate_retract_gear_valve"]);
copiedState.con_stop_stimulate_retract_gear_valve();
copiedState.stateAccessedVia = "con_stop_stimulate_retract_gear_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stimulate_extend_gear_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stimulate_extend_gear_valve"]);
copiedState.con_stimulate_extend_gear_valve();
copiedState.stateAccessedVia = "con_stimulate_extend_gear_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stop_stimulate_extend_gear_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stop_stimulate_extend_gear_valve"]);
copiedState.con_stop_stimulate_extend_gear_valve();
copiedState.stateAccessedVia = "con_stop_stimulate_extend_gear_valve";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_19 = state._tr_env_start_retracting_first(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_19) {
@@ -1911,6 +1927,7 @@ class ModelChecker {
copiedState.env_start_retracting_first(_tmp_1);
copiedState.stateAccessedVia = "env_start_retracting_first";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_20 = state._tr_env_retract_gear_skip(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_20) {
@@ -1920,6 +1937,7 @@ class ModelChecker {
copiedState.env_retract_gear_skip(_tmp_1);
copiedState.stateAccessedVia = "env_retract_gear_skip";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_21 = state._tr_env_retract_gear_last(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_21) {
@@ -1929,6 +1947,7 @@ class ModelChecker {
copiedState.env_retract_gear_last(_tmp_1);
copiedState.stateAccessedVia = "env_retract_gear_last";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_22 = state._tr_env_start_extending(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_22) {
@@ -1938,6 +1957,7 @@ class ModelChecker {
copiedState.env_start_extending(_tmp_1);
copiedState.stateAccessedVia = "env_start_extending";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_23 = state._tr_env_extend_gear_last(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_23) {
@@ -1947,6 +1967,7 @@ class ModelChecker {
copiedState.env_extend_gear_last(_tmp_1);
copiedState.stateAccessedVia = "env_extend_gear_last";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_24 = state._tr_env_extend_gear_skip(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_24) {
@@ -1956,6 +1977,7 @@ class ModelChecker {
copiedState.env_extend_gear_skip(_tmp_1);
copiedState.stateAccessedVia = "env_extend_gear_skip";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_25 = state._tr_env_start_open_door(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_25) {
@@ -1965,6 +1987,7 @@ class ModelChecker {
copiedState.env_start_open_door(_tmp_1);
copiedState.stateAccessedVia = "env_start_open_door";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_26 = state._tr_env_open_door_last(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_26) {
@@ -1974,6 +1997,7 @@ class ModelChecker {
copiedState.env_open_door_last(_tmp_1);
copiedState.stateAccessedVia = "env_open_door_last";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_27 = state._tr_env_open_door_skip(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_27) {
@@ -1983,6 +2007,7 @@ class ModelChecker {
copiedState.env_open_door_skip(_tmp_1);
copiedState.stateAccessedVia = "env_open_door_skip";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_28 = state._tr_env_start_close_door(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_28) {
@@ -1992,6 +2017,7 @@ class ModelChecker {
copiedState.env_start_close_door(_tmp_1);
copiedState.stateAccessedVia = "env_start_close_door";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_29 = state._tr_env_close_door(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_29) {
@@ -2001,6 +2027,7 @@ class ModelChecker {
copiedState.env_close_door(_tmp_1);
copiedState.stateAccessedVia = "env_close_door";
result.insert(copiedState);
+ transitions += 1;
}
BSet<LandingGear_R6::POSITION> _trid_30 = state._tr_env_close_door_skip(isCaching);
for(const LandingGear_R6::POSITION& param : _trid_30) {
@@ -2010,190 +2037,422 @@ class ModelChecker {
copiedState.env_close_door_skip(_tmp_1);
copiedState.stateAccessedVia = "env_close_door_skip";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_toggle_handle_up(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["toggle_handle_up"]);
copiedState.toggle_handle_up();
copiedState.stateAccessedVia = "toggle_handle_up";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_toggle_handle_down(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["toggle_handle_down"]);
copiedState.toggle_handle_down();
copiedState.stateAccessedVia = "toggle_handle_down";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stimulate_general_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stimulate_general_valve"]);
copiedState.con_stimulate_general_valve();
copiedState.stateAccessedVia = "con_stimulate_general_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_con_stop_stimulate_general_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["con_stop_stimulate_general_valve"]);
copiedState.con_stop_stimulate_general_valve();
copiedState.stateAccessedVia = "con_stop_stimulate_general_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_evn_open_general_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["evn_open_general_valve"]);
copiedState.evn_open_general_valve();
copiedState.stateAccessedVia = "evn_open_general_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_evn_close_general_valve(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["evn_close_general_valve"]);
copiedState.evn_close_general_valve();
copiedState.stateAccessedVia = "evn_close_general_valve";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_env_close_analogical_switch(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["env_close_analogical_switch"]);
copiedState.env_close_analogical_switch();
copiedState.stateAccessedVia = "env_close_analogical_switch";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_env_open_analogical_switch(isCaching)) {
LandingGear_R6 copiedState = state._copy(guardDependency["env_open_analogical_switch"]);
copiedState.env_open_analogical_switch();
copiedState.stateAccessedVia = "env_open_analogical_switch";
result.insert(copiedState);
+ transitions += 1;
}
return result;
}
bool invariantViolated(const LandingGear_R6& state) {
+ std::unordered_set<string> dependentInvariantsOfState;
+ if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
if(isCaching) {
- std::unordered_set<string> dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_1()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_2") == dependentInvariantsOfState.end()) {
if(!state._check_inv_2()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_2()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_3") == dependentInvariantsOfState.end()) {
if(!state._check_inv_3()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_3()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_4") == dependentInvariantsOfState.end()) {
if(!state._check_inv_4()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_4()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_5") == dependentInvariantsOfState.end()) {
if(!state._check_inv_5()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_5()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_6") == dependentInvariantsOfState.end()) {
if(!state._check_inv_6()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_6()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_7") == dependentInvariantsOfState.end()) {
if(!state._check_inv_7()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_7()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_8") == dependentInvariantsOfState.end()) {
if(!state._check_inv_8()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_8()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_9") == dependentInvariantsOfState.end()) {
if(!state._check_inv_9()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_9()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_10") == dependentInvariantsOfState.end()) {
if(!state._check_inv_10()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_10()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_11") == dependentInvariantsOfState.end()) {
if(!state._check_inv_11()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_11()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_12") == dependentInvariantsOfState.end()) {
if(!state._check_inv_12()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_12()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_13") == dependentInvariantsOfState.end()) {
if(!state._check_inv_13()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_13()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_14") == dependentInvariantsOfState.end()) {
if(!state._check_inv_14()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_14()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_15") == dependentInvariantsOfState.end()) {
if(!state._check_inv_15()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_15()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_16") == dependentInvariantsOfState.end()) {
if(!state._check_inv_16()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_16()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_17") == dependentInvariantsOfState.end()) {
if(!state._check_inv_17()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_17()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_18") == dependentInvariantsOfState.end()) {
if(!state._check_inv_18()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_18()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_19") == dependentInvariantsOfState.end()) {
if(!state._check_inv_19()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_19" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_19()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_19" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_20") == dependentInvariantsOfState.end()) {
if(!state._check_inv_20()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_20" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_20()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_20" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_21") == dependentInvariantsOfState.end()) {
if(!state._check_inv_21()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_21" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_21()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_21" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_22") == dependentInvariantsOfState.end()) {
if(!state._check_inv_22()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_22" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_22()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_22" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_23") == dependentInvariantsOfState.end()) {
if(!state._check_inv_23()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_23" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_23()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_23" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_24") == dependentInvariantsOfState.end()) {
if(!state._check_inv_24()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_24" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_24()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_24" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_25") == dependentInvariantsOfState.end()) {
if(!state._check_inv_25()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_25" << "\n";
+ return true;
}
}
- return false;
+ } else {
+ if(!state._check_inv_25()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_25" << "\n";
+ return true;
+ }
}
- return !(state._check_inv_1() && state._check_inv_2() && state._check_inv_3() && state._check_inv_4() && state._check_inv_5() && state._check_inv_6() && state._check_inv_7() && state._check_inv_8() && state._check_inv_9() && state._check_inv_10() && state._check_inv_11() && state._check_inv_12() && state._check_inv_13() && state._check_inv_14() && state._check_inv_15() && state._check_inv_16() && state._check_inv_17() && state._check_inv_18() && state._check_inv_19() && state._check_inv_20() && state._check_inv_21() && state._check_inv_22() && state._check_inv_23() && state._check_inv_24() && state._check_inv_25());
+
+ return false;
}
diff --git a/benchmarks/model_checking/C++/Lift_MC_Large.cpp b/benchmarks/model_checking/C++/Lift_MC_Large.cpp
index f376dcfea..cb8c9bbae 100644
--- a/benchmarks/model_checking/C++/Lift_MC_Large.cpp
+++ b/benchmarks/model_checking/C++/Lift_MC_Large.cpp
@@ -228,7 +228,6 @@ class ModelChecker {
Lift_MC_Large state = next();
std::unordered_set<Lift_MC_Large, Lift_MC_Large::Hash, Lift_MC_Large::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
@@ -281,7 +280,6 @@ class ModelChecker {
Lift_MC_Large state = next();
std::packaged_task<void()> task([&, state] {
std::unordered_set<Lift_MC_Large, Lift_MC_Large::Hash, Lift_MC_Large::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
{
@@ -376,7 +374,7 @@ class ModelChecker {
return state;
}
}
- }
+ };
}
std::unordered_set<Lift_MC_Large, Lift_MC_Large::Hash, Lift_MC_Large::HashEqual> generateNextStates(const Lift_MC_Large& state) {
@@ -386,33 +384,51 @@ class ModelChecker {
copiedState.inc();
copiedState.stateAccessedVia = "inc";
result.insert(copiedState);
+ transitions += 1;
}
if(state._tr_dec(isCaching)) {
Lift_MC_Large copiedState = state._copy(guardDependency["dec"]);
copiedState.dec();
copiedState.stateAccessedVia = "dec";
result.insert(copiedState);
+ transitions += 1;
}
return result;
}
bool invariantViolated(const Lift_MC_Large& state) {
+ std::unordered_set<string> dependentInvariantsOfState;
+ if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
if(isCaching) {
- std::unordered_set<string> dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_1()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_2") == dependentInvariantsOfState.end()) {
if(!state._check_inv_2()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
}
}
- return false;
+ } else {
+ if(!state._check_inv_2()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
+ }
}
- return !(state._check_inv_1() && state._check_inv_2());
+
+ return false;
}
diff --git a/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp b/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp
index 28efdeae2..b08328bc8 100644
--- a/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp
+++ b/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp
@@ -494,7 +494,6 @@ class Train1_Lukas_POR_v3 {
}
}
-
return (_ic_boolean_8).booleanValue();
}
@@ -510,7 +509,6 @@ class Train1_Lukas_POR_v3 {
}
}
-
if(!(_ic_boolean_9).booleanValue()) {
_ic_boolean_10 = BBoolean(false);
break;
@@ -518,7 +516,6 @@ class Train1_Lukas_POR_v3 {
}
}
-
return (_ic_boolean_10).booleanValue();
}
@@ -534,7 +531,6 @@ class Train1_Lukas_POR_v3 {
}
}
-
return (_ic_boolean_11).booleanValue();
}
@@ -559,7 +555,6 @@ class Train1_Lukas_POR_v3 {
}
}
-
return (_ic_boolean_12).booleanValue();
}
@@ -593,7 +588,6 @@ class Train1_Lukas_POR_v3 {
}
}
-
return (_ic_boolean_13).booleanValue();
}
@@ -633,11 +627,11 @@ class Train1_Lukas_POR_v3 {
}
friend bool operator ==(const Train1_Lukas_POR_v3& o1, const Train1_Lukas_POR_v3& o2) {
- return o1._get_LBT() == o2._get_LBT() && o1._get_TRK() == o2._get_TRK() && o1._get_frm() == o2._get_frm() && o1._get_OCC() == o2._get_OCC() && o1._get_resbl() == o2._get_resbl() && o1._get_resrt() == o2._get_resrt() && o1._get_rsrtbl() == o2._get_rsrtbl();
+ return o1._get_fst() == o2._get_fst() && o1._get_lst() == o2._get_lst() && o1._get_nxt() == o2._get_nxt() && o1._get_rtbl() == o2._get_rtbl() && o1._get_LBT() == o2._get_LBT() && o1._get_TRK() == o2._get_TRK() && o1._get_frm() == o2._get_frm() && o1._get_OCC() == o2._get_OCC() && o1._get_resbl() == o2._get_resbl() && o1._get_resrt() == o2._get_resrt() && o1._get_rsrtbl() == o2._get_rsrtbl();
}
friend bool operator !=(const Train1_Lukas_POR_v3& o1, const Train1_Lukas_POR_v3& o2) {
- return o1._get_LBT() != o2._get_LBT() || o1._get_TRK() != o2._get_TRK() || o1._get_frm() != o2._get_frm() || o1._get_OCC() != o2._get_OCC() || o1._get_resbl() != o2._get_resbl() || o1._get_resrt() != o2._get_resrt() || o1._get_rsrtbl() != o2._get_rsrtbl();
+ return o1._get_fst() != o2._get_fst() || o1._get_lst() != o2._get_lst() || o1._get_nxt() != o2._get_nxt() || o1._get_rtbl() != o2._get_rtbl() || o1._get_LBT() != o2._get_LBT() || o1._get_TRK() != o2._get_TRK() || o1._get_frm() != o2._get_frm() || o1._get_OCC() != o2._get_OCC() || o1._get_resbl() != o2._get_resbl() || o1._get_resrt() != o2._get_resrt() || o1._get_rsrtbl() != o2._get_rsrtbl();
}
int hashCode() const {
@@ -745,7 +739,6 @@ class ModelChecker {
Train1_Lukas_POR_v3 state = next();
std::unordered_set<Train1_Lukas_POR_v3, Train1_Lukas_POR_v3::Hash, Train1_Lukas_POR_v3::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
@@ -798,7 +791,6 @@ class ModelChecker {
Train1_Lukas_POR_v3 state = next();
std::packaged_task<void()> task([&, state] {
std::unordered_set<Train1_Lukas_POR_v3, Train1_Lukas_POR_v3::Hash, Train1_Lukas_POR_v3::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
{
@@ -905,7 +897,7 @@ class ModelChecker {
return state;
}
}
- }
+ };
}
std::unordered_set<Train1_Lukas_POR_v3, Train1_Lukas_POR_v3::Hash, Train1_Lukas_POR_v3::HashEqual> generateNextStates(const Train1_Lukas_POR_v3& state) {
@@ -918,6 +910,7 @@ class ModelChecker {
copiedState.route_reservation(_tmp_1);
copiedState.stateAccessedVia = "route_reservation";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train1_Lukas_POR_v3::ROUTES> _trid_2 = state._tr_route_freeing(isCaching);
for(const Train1_Lukas_POR_v3::ROUTES& param : _trid_2) {
@@ -927,6 +920,7 @@ class ModelChecker {
copiedState.route_freeing(_tmp_1);
copiedState.stateAccessedVia = "route_freeing";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train1_Lukas_POR_v3::ROUTES> _trid_3 = state._tr_FRONT_MOVE_1(isCaching);
for(const Train1_Lukas_POR_v3::ROUTES& param : _trid_3) {
@@ -936,6 +930,7 @@ class ModelChecker {
copiedState.FRONT_MOVE_1(_tmp_1);
copiedState.stateAccessedVia = "FRONT_MOVE_1";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train1_Lukas_POR_v3::BLOCKS> _trid_4 = state._tr_FRONT_MOVE_2(isCaching);
for(const Train1_Lukas_POR_v3::BLOCKS& param : _trid_4) {
@@ -945,6 +940,7 @@ class ModelChecker {
copiedState.FRONT_MOVE_2(_tmp_1);
copiedState.stateAccessedVia = "FRONT_MOVE_2";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train1_Lukas_POR_v3::BLOCKS> _trid_5 = state._tr_BACK_MOVE_1(isCaching);
for(const Train1_Lukas_POR_v3::BLOCKS& param : _trid_5) {
@@ -954,6 +950,7 @@ class ModelChecker {
copiedState.BACK_MOVE_1(_tmp_1);
copiedState.stateAccessedVia = "BACK_MOVE_1";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train1_Lukas_POR_v3::BLOCKS> _trid_6 = state._tr_BACK_MOVE_2(isCaching);
for(const Train1_Lukas_POR_v3::BLOCKS& param : _trid_6) {
@@ -963,6 +960,7 @@ class ModelChecker {
copiedState.BACK_MOVE_2(_tmp_1);
copiedState.stateAccessedVia = "BACK_MOVE_2";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train1_Lukas_POR_v3::ROUTES> _trid_7 = state._tr_point_positionning(isCaching);
for(const Train1_Lukas_POR_v3::ROUTES& param : _trid_7) {
@@ -972,6 +970,7 @@ class ModelChecker {
copiedState.point_positionning(_tmp_1);
copiedState.stateAccessedVia = "point_positionning";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train1_Lukas_POR_v3::ROUTES> _trid_8 = state._tr_route_formation(isCaching);
for(const Train1_Lukas_POR_v3::ROUTES& param : _trid_8) {
@@ -981,77 +980,184 @@ class ModelChecker {
copiedState.route_formation(_tmp_1);
copiedState.stateAccessedVia = "route_formation";
result.insert(copiedState);
+ transitions += 1;
}
return result;
}
bool invariantViolated(const Train1_Lukas_POR_v3& state) {
+ std::unordered_set<string> dependentInvariantsOfState;
+ if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
if(isCaching) {
- std::unordered_set<string> dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_1()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_2") == dependentInvariantsOfState.end()) {
if(!state._check_inv_2()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_2()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_3") == dependentInvariantsOfState.end()) {
if(!state._check_inv_3()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_3()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_4") == dependentInvariantsOfState.end()) {
if(!state._check_inv_4()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_4()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_5") == dependentInvariantsOfState.end()) {
if(!state._check_inv_5()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_5()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_6") == dependentInvariantsOfState.end()) {
if(!state._check_inv_6()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_6()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_7") == dependentInvariantsOfState.end()) {
if(!state._check_inv_7()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_7()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_8") == dependentInvariantsOfState.end()) {
if(!state._check_inv_8()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_8()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_9") == dependentInvariantsOfState.end()) {
if(!state._check_inv_9()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_9()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_10") == dependentInvariantsOfState.end()) {
if(!state._check_inv_10()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_10()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_11") == dependentInvariantsOfState.end()) {
if(!state._check_inv_11()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_11()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_12") == dependentInvariantsOfState.end()) {
if(!state._check_inv_12()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
}
}
- return false;
+ } else {
+ if(!state._check_inv_12()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
+ }
}
- return !(state._check_inv_1() && state._check_inv_2() && state._check_inv_3() && state._check_inv_4() && state._check_inv_5() && state._check_inv_6() && state._check_inv_7() && state._check_inv_8() && state._check_inv_9() && state._check_inv_10() && state._check_inv_11() && state._check_inv_12());
+
+ return false;
}
diff --git a/benchmarks/model_checking/C++/Train_1_beebook_deterministic_MC_POR_v2.cpp b/benchmarks/model_checking/C++/Train_1_beebook_deterministic_MC_POR_v2.cpp
index 6c76d2f72..cb7735f7e 100644
--- a/benchmarks/model_checking/C++/Train_1_beebook_deterministic_MC_POR_v2.cpp
+++ b/benchmarks/model_checking/C++/Train_1_beebook_deterministic_MC_POR_v2.cpp
@@ -241,7 +241,6 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
}
-
rtbl = _ic_set_0;
resrt = (BSet<ROUTES >());
resbl = (BSet<BLOCKS >());
@@ -518,7 +517,6 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
}
-
return (_ic_boolean_9).booleanValue();
}
@@ -534,7 +532,6 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
}
-
if(!(_ic_boolean_10).booleanValue()) {
_ic_boolean_11 = BBoolean(false);
break;
@@ -542,7 +539,6 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
}
-
return (_ic_boolean_11).booleanValue();
}
@@ -558,7 +554,6 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
}
-
return (_ic_boolean_12).booleanValue();
}
@@ -583,7 +578,6 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
}
-
return (_ic_boolean_13).booleanValue();
}
@@ -617,7 +611,6 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
}
-
return (_ic_boolean_14).booleanValue();
}
@@ -657,11 +650,11 @@ class Train_1_beebook_deterministic_MC_POR_v2 {
}
friend bool operator ==(const Train_1_beebook_deterministic_MC_POR_v2& o1, const Train_1_beebook_deterministic_MC_POR_v2& o2) {
- return o1._get_LBT() == o2._get_LBT() && o1._get_TRK() == o2._get_TRK() && o1._get_frm() == o2._get_frm() && o1._get_OCC() == o2._get_OCC() && o1._get_resbl() == o2._get_resbl() && o1._get_resrt() == o2._get_resrt() && o1._get_rsrtbl() == o2._get_rsrtbl();
+ return o1._get_fst() == o2._get_fst() && o1._get_lst() == o2._get_lst() && o1._get_nxt() == o2._get_nxt() && o1._get_rtbl() == o2._get_rtbl() && o1._get_LBT() == o2._get_LBT() && o1._get_TRK() == o2._get_TRK() && o1._get_frm() == o2._get_frm() && o1._get_OCC() == o2._get_OCC() && o1._get_resbl() == o2._get_resbl() && o1._get_resrt() == o2._get_resrt() && o1._get_rsrtbl() == o2._get_rsrtbl();
}
friend bool operator !=(const Train_1_beebook_deterministic_MC_POR_v2& o1, const Train_1_beebook_deterministic_MC_POR_v2& o2) {
- return o1._get_LBT() != o2._get_LBT() || o1._get_TRK() != o2._get_TRK() || o1._get_frm() != o2._get_frm() || o1._get_OCC() != o2._get_OCC() || o1._get_resbl() != o2._get_resbl() || o1._get_resrt() != o2._get_resrt() || o1._get_rsrtbl() != o2._get_rsrtbl();
+ return o1._get_fst() != o2._get_fst() || o1._get_lst() != o2._get_lst() || o1._get_nxt() != o2._get_nxt() || o1._get_rtbl() != o2._get_rtbl() || o1._get_LBT() != o2._get_LBT() || o1._get_TRK() != o2._get_TRK() || o1._get_frm() != o2._get_frm() || o1._get_OCC() != o2._get_OCC() || o1._get_resbl() != o2._get_resbl() || o1._get_resrt() != o2._get_resrt() || o1._get_rsrtbl() != o2._get_rsrtbl();
}
int hashCode() const {
@@ -769,7 +762,6 @@ class ModelChecker {
Train_1_beebook_deterministic_MC_POR_v2 state = next();
std::unordered_set<Train_1_beebook_deterministic_MC_POR_v2, Train_1_beebook_deterministic_MC_POR_v2::Hash, Train_1_beebook_deterministic_MC_POR_v2::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
@@ -822,7 +814,6 @@ class ModelChecker {
Train_1_beebook_deterministic_MC_POR_v2 state = next();
std::packaged_task<void()> task([&, state] {
std::unordered_set<Train_1_beebook_deterministic_MC_POR_v2, Train_1_beebook_deterministic_MC_POR_v2::Hash, Train_1_beebook_deterministic_MC_POR_v2::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
{
@@ -929,7 +920,7 @@ class ModelChecker {
return state;
}
}
- }
+ };
}
std::unordered_set<Train_1_beebook_deterministic_MC_POR_v2, Train_1_beebook_deterministic_MC_POR_v2::Hash, Train_1_beebook_deterministic_MC_POR_v2::HashEqual> generateNextStates(const Train_1_beebook_deterministic_MC_POR_v2& state) {
@@ -942,6 +933,7 @@ class ModelChecker {
copiedState.route_reservation(_tmp_1);
copiedState.stateAccessedVia = "route_reservation";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train_1_beebook_deterministic_MC_POR_v2::ROUTES> _trid_2 = state._tr_route_freeing(isCaching);
for(const Train_1_beebook_deterministic_MC_POR_v2::ROUTES& param : _trid_2) {
@@ -951,6 +943,7 @@ class ModelChecker {
copiedState.route_freeing(_tmp_1);
copiedState.stateAccessedVia = "route_freeing";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train_1_beebook_deterministic_MC_POR_v2::ROUTES> _trid_3 = state._tr_FRONT_MOVE_1(isCaching);
for(const Train_1_beebook_deterministic_MC_POR_v2::ROUTES& param : _trid_3) {
@@ -960,6 +953,7 @@ class ModelChecker {
copiedState.FRONT_MOVE_1(_tmp_1);
copiedState.stateAccessedVia = "FRONT_MOVE_1";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train_1_beebook_deterministic_MC_POR_v2::BLOCKS> _trid_4 = state._tr_FRONT_MOVE_2(isCaching);
for(const Train_1_beebook_deterministic_MC_POR_v2::BLOCKS& param : _trid_4) {
@@ -969,6 +963,7 @@ class ModelChecker {
copiedState.FRONT_MOVE_2(_tmp_1);
copiedState.stateAccessedVia = "FRONT_MOVE_2";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train_1_beebook_deterministic_MC_POR_v2::BLOCKS> _trid_5 = state._tr_BACK_MOVE_1(isCaching);
for(const Train_1_beebook_deterministic_MC_POR_v2::BLOCKS& param : _trid_5) {
@@ -978,6 +973,7 @@ class ModelChecker {
copiedState.BACK_MOVE_1(_tmp_1);
copiedState.stateAccessedVia = "BACK_MOVE_1";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train_1_beebook_deterministic_MC_POR_v2::BLOCKS> _trid_6 = state._tr_BACK_MOVE_2(isCaching);
for(const Train_1_beebook_deterministic_MC_POR_v2::BLOCKS& param : _trid_6) {
@@ -987,6 +983,7 @@ class ModelChecker {
copiedState.BACK_MOVE_2(_tmp_1);
copiedState.stateAccessedVia = "BACK_MOVE_2";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train_1_beebook_deterministic_MC_POR_v2::ROUTES> _trid_7 = state._tr_point_positionning(isCaching);
for(const Train_1_beebook_deterministic_MC_POR_v2::ROUTES& param : _trid_7) {
@@ -996,6 +993,7 @@ class ModelChecker {
copiedState.point_positionning(_tmp_1);
copiedState.stateAccessedVia = "point_positionning";
result.insert(copiedState);
+ transitions += 1;
}
BSet<Train_1_beebook_deterministic_MC_POR_v2::ROUTES> _trid_8 = state._tr_route_formation(isCaching);
for(const Train_1_beebook_deterministic_MC_POR_v2::ROUTES& param : _trid_8) {
@@ -1005,77 +1003,184 @@ class ModelChecker {
copiedState.route_formation(_tmp_1);
copiedState.stateAccessedVia = "route_formation";
result.insert(copiedState);
+ transitions += 1;
}
return result;
}
bool invariantViolated(const Train_1_beebook_deterministic_MC_POR_v2& state) {
+ std::unordered_set<string> dependentInvariantsOfState;
+ if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
if(isCaching) {
- std::unordered_set<string> dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_1()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_2") == dependentInvariantsOfState.end()) {
if(!state._check_inv_2()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_2()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_3") == dependentInvariantsOfState.end()) {
if(!state._check_inv_3()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_3()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_4") == dependentInvariantsOfState.end()) {
if(!state._check_inv_4()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_4()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_5") == dependentInvariantsOfState.end()) {
if(!state._check_inv_5()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_5()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_6") == dependentInvariantsOfState.end()) {
if(!state._check_inv_6()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_6()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_7") == dependentInvariantsOfState.end()) {
if(!state._check_inv_7()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_7()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_8") == dependentInvariantsOfState.end()) {
if(!state._check_inv_8()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_8()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_9") == dependentInvariantsOfState.end()) {
if(!state._check_inv_9()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_9()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_10") == dependentInvariantsOfState.end()) {
if(!state._check_inv_10()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_10()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_11") == dependentInvariantsOfState.end()) {
if(!state._check_inv_11()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_11()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_12") == dependentInvariantsOfState.end()) {
if(!state._check_inv_12()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
}
}
- return false;
+ } else {
+ if(!state._check_inv_12()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
+ }
}
- return !(state._check_inv_1() && state._check_inv_2() && state._check_inv_3() && state._check_inv_4() && state._check_inv_5() && state._check_inv_6() && state._check_inv_7() && state._check_inv_8() && state._check_inv_9() && state._check_inv_10() && state._check_inv_11() && state._check_inv_12());
+
+ return false;
}
diff --git a/benchmarks/model_checking/C++/nota_v2.cpp b/benchmarks/model_checking/C++/nota_v2.cpp
index a4ebf27e7..ce794ed86 100644
--- a/benchmarks/model_checking/C++/nota_v2.cpp
+++ b/benchmarks/model_checking/C++/nota_v2.cpp
@@ -421,18 +421,18 @@ class nota_v2 {
}
};
- class _Struct1 : public BStruct {
+ class _Struct3 : public BStruct {
private:
BSet<SID > sid;
- RM_ERROR_CODES err;
+ IN_ERROR_CODES err;
public:
- typedef _Struct1 current_type;
+ typedef _Struct3 current_type;
typedef void value_type;
typedef void left_type;
typedef void right_type;
- _Struct1(const BSet<SID >& sid, const RM_ERROR_CODES& err) {
+ _Struct3(const BSet<SID >& sid, const IN_ERROR_CODES& err) {
this->sid = sid;
this->err = err;
}
@@ -441,43 +441,43 @@ class nota_v2 {
return this->sid;
}
- RM_ERROR_CODES get_err() {
+ IN_ERROR_CODES get_err() {
return this->err;
}
- _Struct1 override_sid(const BSet<SID >& sid) {
- return _Struct1(sid, err);
+ _Struct3 override_sid(const BSet<SID >& sid) {
+ return _Struct3(sid, err);
}
- _Struct1 override_err(const RM_ERROR_CODES& err) {
- return _Struct1(sid, err);
+ _Struct3 override_err(const IN_ERROR_CODES& err) {
+ return _Struct3(sid, err);
}
- _Struct1() {
+ _Struct3() {
}
- void operator =(const _Struct1& other) {
+ void operator =(const _Struct3& other) {
this->sid = other.sid;
this->err = other.err;
}
- BBoolean equal(const _Struct1& o) const {
+ BBoolean equal(const _Struct3& o) const {
return this->sid == o.sid && this->err == o.err;
}
- BBoolean unequal(const _Struct1& o) const {
+ BBoolean unequal(const _Struct3& o) const {
return this->sid != o.sid || this->err != o.err;
}
- friend bool operator ==(const _Struct1& p1, const _Struct1& p2) {
+ friend bool operator ==(const _Struct3& p1, const _Struct3& p2) {
return (p1.equal(p2)).booleanValue();
}
- friend bool operator !=(const _Struct1& p1, const _Struct1& p2) {
+ friend bool operator !=(const _Struct3& p1, const _Struct3& p2) {
return (p1.unequal(p2)).booleanValue();
}
- friend std::ostream& operator<<(std::ostream &strm, const _Struct1& e) {
+ friend std::ostream& operator<<(std::ostream &strm, const _Struct3& e) {
strm << "(";
strm << "sid : ";
strm << e.sid;
@@ -495,66 +495,66 @@ class nota_v2 {
}
};
- class _Struct5 : public BStruct {
+ class _Struct1 : public BStruct {
private:
- BSet<SOCKET > soc;
- IN_ERROR_CODES err;
+ BSet<SID > sid;
+ RM_ERROR_CODES err;
public:
- typedef _Struct5 current_type;
+ typedef _Struct1 current_type;
typedef void value_type;
typedef void left_type;
typedef void right_type;
- _Struct5(const BSet<SOCKET >& soc, const IN_ERROR_CODES& err) {
- this->soc = soc;
+ _Struct1(const BSet<SID >& sid, const RM_ERROR_CODES& err) {
+ this->sid = sid;
this->err = err;
}
- BSet<SOCKET > get_soc() {
- return this->soc;
+ BSet<SID > get_sid() {
+ return this->sid;
}
- IN_ERROR_CODES get_err() {
+ RM_ERROR_CODES get_err() {
return this->err;
}
- _Struct5 override_soc(const BSet<SOCKET >& soc) {
- return _Struct5(soc, err);
+ _Struct1 override_sid(const BSet<SID >& sid) {
+ return _Struct1(sid, err);
}
- _Struct5 override_err(const IN_ERROR_CODES& err) {
- return _Struct5(soc, err);
+ _Struct1 override_err(const RM_ERROR_CODES& err) {
+ return _Struct1(sid, err);
}
- _Struct5() {
+ _Struct1() {
}
- void operator =(const _Struct5& other) {
- this->soc = other.soc;
+ void operator =(const _Struct1& other) {
+ this->sid = other.sid;
this->err = other.err;
}
- BBoolean equal(const _Struct5& o) const {
- return this->soc == o.soc && this->err == o.err;
+ BBoolean equal(const _Struct1& o) const {
+ return this->sid == o.sid && this->err == o.err;
}
- BBoolean unequal(const _Struct5& o) const {
- return this->soc != o.soc || this->err != o.err;
+ BBoolean unequal(const _Struct1& o) const {
+ return this->sid != o.sid || this->err != o.err;
}
- friend bool operator ==(const _Struct5& p1, const _Struct5& p2) {
+ friend bool operator ==(const _Struct1& p1, const _Struct1& p2) {
return (p1.equal(p2)).booleanValue();
}
- friend bool operator !=(const _Struct5& p1, const _Struct5& p2) {
+ friend bool operator !=(const _Struct1& p1, const _Struct1& p2) {
return (p1.unequal(p2)).booleanValue();
}
- friend std::ostream& operator<<(std::ostream &strm, const _Struct5& e) {
+ friend std::ostream& operator<<(std::ostream &strm, const _Struct1& e) {
strm << "(";
- strm << "soc : ";
- strm << e.soc;
+ strm << "sid : ";
+ strm << e.sid;
strm << "err : ";
strm << e.err;
strm << ")";
@@ -563,72 +563,72 @@ class nota_v2 {
int hashCode() const {
int result = 1;
- result = 31 * result + (soc.hashCode() << 1);
+ result = 31 * result + (sid.hashCode() << 1);
result = 31 * result + (err.hashCode() << 1);
return result;
}
};
- class _Struct3 : public BStruct {
+ class _Struct5 : public BStruct {
private:
- BSet<SID > sid;
+ BSet<SOCKET > soc;
IN_ERROR_CODES err;
public:
- typedef _Struct3 current_type;
+ typedef _Struct5 current_type;
typedef void value_type;
typedef void left_type;
typedef void right_type;
- _Struct3(const BSet<SID >& sid, const IN_ERROR_CODES& err) {
- this->sid = sid;
+ _Struct5(const BSet<SOCKET >& soc, const IN_ERROR_CODES& err) {
+ this->soc = soc;
this->err = err;
}
- BSet<SID > get_sid() {
- return this->sid;
+ BSet<SOCKET > get_soc() {
+ return this->soc;
}
IN_ERROR_CODES get_err() {
return this->err;
}
- _Struct3 override_sid(const BSet<SID >& sid) {
- return _Struct3(sid, err);
+ _Struct5 override_soc(const BSet<SOCKET >& soc) {
+ return _Struct5(soc, err);
}
- _Struct3 override_err(const IN_ERROR_CODES& err) {
- return _Struct3(sid, err);
+ _Struct5 override_err(const IN_ERROR_CODES& err) {
+ return _Struct5(soc, err);
}
- _Struct3() {
+ _Struct5() {
}
- void operator =(const _Struct3& other) {
- this->sid = other.sid;
+ void operator =(const _Struct5& other) {
+ this->soc = other.soc;
this->err = other.err;
}
- BBoolean equal(const _Struct3& o) const {
- return this->sid == o.sid && this->err == o.err;
+ BBoolean equal(const _Struct5& o) const {
+ return this->soc == o.soc && this->err == o.err;
}
- BBoolean unequal(const _Struct3& o) const {
- return this->sid != o.sid || this->err != o.err;
+ BBoolean unequal(const _Struct5& o) const {
+ return this->soc != o.soc || this->err != o.err;
}
- friend bool operator ==(const _Struct3& p1, const _Struct3& p2) {
+ friend bool operator ==(const _Struct5& p1, const _Struct5& p2) {
return (p1.equal(p2)).booleanValue();
}
- friend bool operator !=(const _Struct3& p1, const _Struct3& p2) {
+ friend bool operator !=(const _Struct5& p1, const _Struct5& p2) {
return (p1.unequal(p2)).booleanValue();
}
- friend std::ostream& operator<<(std::ostream &strm, const _Struct3& e) {
+ friend std::ostream& operator<<(std::ostream &strm, const _Struct5& e) {
strm << "(";
- strm << "sid : ";
- strm << e.sid;
+ strm << "soc : ";
+ strm << e.soc;
strm << "err : ";
strm << e.err;
strm << ")";
@@ -637,7 +637,7 @@ class nota_v2 {
int hashCode() const {
int result = 1;
- result = 31 * result + (sid.hashCode() << 1);
+ result = 31 * result + (soc.hashCode() << 1);
result = 31 * result + (err.hashCode() << 1);
return result;
}
@@ -1241,7 +1241,6 @@ class nota_v2 {
}
}
-
return (_ic_boolean_14).booleanValue();
}
@@ -1462,7 +1461,6 @@ class ModelChecker {
nota_v2 state = next();
std::unordered_set<nota_v2, nota_v2::Hash, nota_v2::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
@@ -1515,7 +1513,6 @@ class ModelChecker {
nota_v2 state = next();
std::packaged_task<void()> task([&, state] {
std::unordered_set<nota_v2, nota_v2::Hash, nota_v2::HashEqual> nextStates = generateNextStates(state);
- transitions += nextStates.size();
for(auto& nextState : nextStates) {
{
@@ -1634,7 +1631,7 @@ class ModelChecker {
return state;
}
}
- }
+ };
}
std::unordered_set<nota_v2, nota_v2::Hash, nota_v2::HashEqual> generateNextStates(const nota_v2& state) {
@@ -1647,6 +1644,7 @@ class ModelChecker {
copiedState.constructor_interconnectNode(_tmp_1);
copiedState.stateAccessedVia = "constructor_interconnectNode";
result.insert(copiedState);
+ transitions += 1;
}
BSet<nota_v2::RESOURCEMANAGER> _trid_2 = state._tr_constructor_resourceManager(isCaching);
for(const nota_v2::RESOURCEMANAGER& param : _trid_2) {
@@ -1656,6 +1654,7 @@ class ModelChecker {
copiedState.constructor_resourceManager(_tmp_1);
copiedState.stateAccessedVia = "constructor_resourceManager";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SERVICE >> _trid_3 = state._tr_constructor_service(isCaching);
for(const BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SERVICE >& param : _trid_3) {
@@ -1666,6 +1665,7 @@ class ModelChecker {
copiedState.constructor_service(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "constructor_service";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SID >, nota_v2::SID >, nota_v2::SOCKET >> _trid_4 = state._tr_constructor_socket(isCaching);
for(const BTuple<BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SID >, nota_v2::SID >, nota_v2::SOCKET >& param : _trid_4) {
@@ -1680,6 +1680,7 @@ class ModelChecker {
copiedState.constructor_socket(_tmp_6, _tmp_5, _tmp_3, _tmp_1);
copiedState.stateAccessedVia = "constructor_socket";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >, nota_v2::INTERCONNECTNODE >> _trid_5 = state._tr_rm_register(isCaching);
for(const BTuple<BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >, nota_v2::INTERCONNECTNODE >& param : _trid_5) {
@@ -1692,6 +1693,7 @@ class ModelChecker {
copiedState.rm_register(_tmp_4, _tmp_3, _tmp_1);
copiedState.stateAccessedVia = "rm_register";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >, nota_v2::INTERCONNECTNODE >> _trid_6 = state._tr_rm_deregister(isCaching);
for(const BTuple<BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >, nota_v2::INTERCONNECTNODE >& param : _trid_6) {
@@ -1704,6 +1706,7 @@ class ModelChecker {
copiedState.rm_deregister(_tmp_4, _tmp_3, _tmp_1);
copiedState.stateAccessedVia = "rm_deregister";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >> _trid_7 = state._tr_rm_getSid(isCaching);
for(const BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >& param : _trid_7) {
@@ -1714,6 +1717,7 @@ class ModelChecker {
copiedState.rm_getSid(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "rm_getSid";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >> _trid_8 = state._tr_rm_getSid_Not_Found(isCaching);
for(const BTuple<nota_v2::RESOURCEMANAGER, nota_v2::SERVICE >& param : _trid_8) {
@@ -1724,6 +1728,7 @@ class ModelChecker {
copiedState.rm_getSid_Not_Found(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "rm_getSid_Not_Found";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::RESOURCEMANAGER >> _trid_9 = state._tr_in_announceResourceManager(isCaching);
for(const BTuple<nota_v2::INTERCONNECTNODE, nota_v2::RESOURCEMANAGER >& param : _trid_9) {
@@ -1734,6 +1739,7 @@ class ModelChecker {
copiedState.in_announceResourceManager(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "in_announceResourceManager";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SERVICE >, nota_v2::SID >> _trid_10 = state._tr_in_register_success(isCaching);
for(const BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SERVICE >, nota_v2::SID >& param : _trid_10) {
@@ -1746,6 +1752,7 @@ class ModelChecker {
copiedState.in_register_success(_tmp_4, _tmp_3, _tmp_1);
copiedState.stateAccessedVia = "in_register_success";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SERVICE >> _trid_11 = state._tr_in_register_failed(isCaching);
for(const BTuple<nota_v2::INTERCONNECTNODE, nota_v2::SERVICE >& param : _trid_11) {
@@ -1756,6 +1763,7 @@ class ModelChecker {
copiedState.in_register_failed(_tmp_2, _tmp_1);
copiedState.stateAccessedVia = "in_register_failed";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BTuple<BTuple<BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::INTERCONNECTNODE >, nota_v2::SOCKET >, nota_v2::SID >, nota_v2::SID >, nota_v2::SOCKET >> _trid_12 = state._tr_in_requestTargetSocket_Granted(isCaching);
for(const BTuple<BTuple<BTuple<BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::INTERCONNECTNODE >, nota_v2::SOCKET >, nota_v2::SID >, nota_v2::SID >, nota_v2::SOCKET >& param : _trid_12) {
@@ -1774,6 +1782,7 @@ class ModelChecker {
copiedState.in_requestTargetSocket_Granted(_tmp_10, _tmp_9, _tmp_7, _tmp_5, _tmp_3, _tmp_1);
copiedState.stateAccessedVia = "in_requestTargetSocket_Granted";
result.insert(copiedState);
+ transitions += 1;
}
BSet<BTuple<BTuple<BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::INTERCONNECTNODE >, nota_v2::SOCKET >, nota_v2::SID >, nota_v2::SID >> _trid_13 = state._tr_in_requestTargetSocket_NotGranted(isCaching);
for(const BTuple<BTuple<BTuple<BTuple<nota_v2::INTERCONNECTNODE, nota_v2::INTERCONNECTNODE >, nota_v2::SOCKET >, nota_v2::SID >, nota_v2::SID >& param : _trid_13) {
@@ -1790,6 +1799,7 @@ class ModelChecker {
copiedState.in_requestTargetSocket_NotGranted(_tmp_8, _tmp_7, _tmp_5, _tmp_3, _tmp_1);
copiedState.stateAccessedVia = "in_requestTargetSocket_NotGranted";
result.insert(copiedState);
+ transitions += 1;
}
BSet<nota_v2::SERVICE> _trid_14 = state._tr_svc_register(isCaching);
for(const nota_v2::SERVICE& param : _trid_14) {
@@ -1799,107 +1809,268 @@ class ModelChecker {
copiedState.svc_register(_tmp_1);
copiedState.stateAccessedVia = "svc_register";
result.insert(copiedState);
+ transitions += 1;
}
return result;
}
bool invariantViolated(const nota_v2& state) {
+ std::unordered_set<string> dependentInvariantsOfState;
+ if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
if(isCaching) {
- std::unordered_set<string> dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_1()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_1" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_2") == dependentInvariantsOfState.end()) {
if(!state._check_inv_2()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_2()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_2" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_3") == dependentInvariantsOfState.end()) {
if(!state._check_inv_3()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_3()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_3" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_4") == dependentInvariantsOfState.end()) {
if(!state._check_inv_4()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_4()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_4" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_5") == dependentInvariantsOfState.end()) {
if(!state._check_inv_5()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_5()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_5" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_6") == dependentInvariantsOfState.end()) {
if(!state._check_inv_6()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_6()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_6" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_7") == dependentInvariantsOfState.end()) {
if(!state._check_inv_7()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_7()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_7" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_8") == dependentInvariantsOfState.end()) {
if(!state._check_inv_8()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_8()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_8" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_9") == dependentInvariantsOfState.end()) {
if(!state._check_inv_9()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_9()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_9" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_10") == dependentInvariantsOfState.end()) {
if(!state._check_inv_10()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_10()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_10" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_11") == dependentInvariantsOfState.end()) {
if(!state._check_inv_11()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_11()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_11" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_12") == dependentInvariantsOfState.end()) {
if(!state._check_inv_12()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_12()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_12" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_13") == dependentInvariantsOfState.end()) {
if(!state._check_inv_13()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_13()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_13" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_14") == dependentInvariantsOfState.end()) {
if(!state._check_inv_14()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_14()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_14" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_15") == dependentInvariantsOfState.end()) {
if(!state._check_inv_15()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_15()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_15" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_16") == dependentInvariantsOfState.end()) {
if(!state._check_inv_16()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_16()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_16" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_17") == dependentInvariantsOfState.end()) {
if(!state._check_inv_17()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
}
}
+ } else {
+ if(!state._check_inv_17()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_17" << "\n";
+ return true;
+ }
+ }
+
+ if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_18") == dependentInvariantsOfState.end()) {
if(!state._check_inv_18()) {
- return false;
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
}
}
- return false;
+ } else {
+ if(!state._check_inv_18()) {
+ cout << "INVARIANT CONJUNCT VIOLATED: _check_inv_18" << "\n";
+ return true;
+ }
}
- return !(state._check_inv_1() && state._check_inv_2() && state._check_inv_3() && state._check_inv_4() && state._check_inv_5() && state._check_inv_6() && state._check_inv_7() && state._check_inv_8() && state._check_inv_9() && state._check_inv_10() && state._check_inv_11() && state._check_inv_12() && state._check_inv_13() && state._check_inv_14() && state._check_inv_15() && state._check_inv_16() && state._check_inv_17() && state._check_inv_18());
+
+ return false;
}
--
GitLab