From 52c71798201cd066bb95a81f910527342a1cf052 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Mon, 12 Jun 2023 14:40:57 +0200
Subject: [PATCH] fixed C++ MC template
---
benchmarks/model_checking/C++/CAN_BUS_tlc.cpp | 2 +-
.../model_checking/C++/Cruise_finite1_deterministic_MC.cpp | 2 +-
benchmarks/model_checking/C++/LandingGear_R6.cpp | 2 +-
benchmarks/model_checking/C++/Lift_MC_Large.cpp | 2 +-
benchmarks/model_checking/C++/Makefile | 6 +++---
benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp | 2 +-
.../C++/Train_1_beebook_deterministic_MC_POR_v2.cpp | 2 +-
benchmarks/model_checking/C++/nota_v2.cpp | 2 +-
.../resources/de/hhu/stups/codegenerator/CppTemplate.stg | 2 +-
9 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp b/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp
index 95ce7b51c..7c74c7f83 100644
--- a/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp
+++ b/benchmarks/model_checking/C++/CAN_BUS_tlc.cpp
@@ -1545,7 +1545,7 @@ class ModelChecker {
bool invariantViolated(const CAN_BUS_tlc& state) {
std::unordered_set<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
diff --git a/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp b/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp
index a6f64d4c7..3b450950b 100644
--- a/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp
+++ b/benchmarks/model_checking/C++/Cruise_finite1_deterministic_MC.cpp
@@ -1558,7 +1558,7 @@ class ModelChecker {
bool invariantViolated(const Cruise_finite1_deterministic_MC& state) {
std::unordered_set<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
diff --git a/benchmarks/model_checking/C++/LandingGear_R6.cpp b/benchmarks/model_checking/C++/LandingGear_R6.cpp
index feb1f0122..c3f0e6113 100644
--- a/benchmarks/model_checking/C++/LandingGear_R6.cpp
+++ b/benchmarks/model_checking/C++/LandingGear_R6.cpp
@@ -2101,7 +2101,7 @@ class ModelChecker {
bool invariantViolated(const LandingGear_R6& state) {
std::unordered_set<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
diff --git a/benchmarks/model_checking/C++/Lift_MC_Large.cpp b/benchmarks/model_checking/C++/Lift_MC_Large.cpp
index cb8c9bbae..fee4a74ce 100644
--- a/benchmarks/model_checking/C++/Lift_MC_Large.cpp
+++ b/benchmarks/model_checking/C++/Lift_MC_Large.cpp
@@ -399,7 +399,7 @@ class ModelChecker {
bool invariantViolated(const Lift_MC_Large& state) {
std::unordered_set<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
diff --git a/benchmarks/model_checking/C++/Makefile b/benchmarks/model_checking/C++/Makefile
index df919d005..942f314ed 100644
--- a/benchmarks/model_checking/C++/Makefile
+++ b/benchmarks/model_checking/C++/Makefile
@@ -2,15 +2,15 @@
.PHONY: build all clean
-all: Lift_MC_Large CAN_BUS_tlc Cruise_finite1_deterministic_MC LandingGear_R6 Train1_Lukas_POR_v3 Train_1_beebook_deterministic_MC_POR_v2 sort_m2_data1000_MC QueensWithEvents_4 QueensWithEvents_8 nota_v2
+all: Lift_MC_Large Cruise_finite1_deterministic_MC LandingGear_R6 CAN_BUS_tlc Train1_Lukas_POR_v3 Train_1_beebook_deterministic_MC_POR_v2 nota_v2 #sort_m2_data1000_MC nota_v2 QueensWithEvents_4 QueensWithEvents_8
build:
cd ../../../btypes_primitives ; ./gradlew -q fatJar ; cp build/libs/btypes_primitives-all.jar ../benchmarks/model_checking/Java/btypes.jar ; cd ../benchmarks/model_checking/Java
CPPC ?= clang++
-CPPFLAGS ?= -std=c++14 -O1 -flto
+CPPFLAGS ?= -std=c++14 -O2 -flto -lboost_system -pthread
STRATEGY=mixed
-THREADS=6
+THREADS=8
CACHING=true
OUTPUT=runtimes.txt
diff --git a/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp b/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp
index b08328bc8..21aa85e72 100644
--- a/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp
+++ b/benchmarks/model_checking/C++/Train1_Lukas_POR_v3.cpp
@@ -988,7 +988,7 @@ class ModelChecker {
bool invariantViolated(const Train1_Lukas_POR_v3& state) {
std::unordered_set<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
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 cb7735f7e..389af6596 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
@@ -1011,7 +1011,7 @@ class ModelChecker {
bool invariantViolated(const Train_1_beebook_deterministic_MC_POR_v2& state) {
std::unordered_set<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
diff --git a/benchmarks/model_checking/C++/nota_v2.cpp b/benchmarks/model_checking/C++/nota_v2.cpp
index ce794ed86..1531aec38 100644
--- a/benchmarks/model_checking/C++/nota_v2.cpp
+++ b/benchmarks/model_checking/C++/nota_v2.cpp
@@ -1817,7 +1817,7 @@ class ModelChecker {
bool invariantViolated(const nota_v2& state) {
std::unordered_set<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
if(isCaching) {
if(dependentInvariantsOfState.find("_check_inv_1") == dependentInvariantsOfState.end()) {
if(!state._check_inv_1()) {
diff --git a/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
index 958aac19d..7cc659cbb 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
@@ -1146,7 +1146,7 @@ model_check_transition_param_assignment(type, param, val, isLhs, oneParameter) :
model_check_invariants(machine, invariantViolated) ::= <<
bool invariantViolated(const <machine>& state) {
std::unordered_set\<string> dependentInvariantsOfState;
- if(isCaching) dependentInvariantsOfState = dependentInvariant[state];
+ if(isCaching) dependentInvariantsOfState = invariantDependency[state.stateAccessedVia];
<invariantViolated; separator="\n">
return false;
}
--
GitLab