diff --git a/README.md b/README.md
index 378941260cebb9871d21423952f83f106986a1d2..03b389fe419fb226da7b9837107fc7d07b8484c0 100644
--- a/README.md
+++ b/README.md
@@ -136,31 +136,31 @@ P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for
### Sets:
-| Set expression or predicate | Meaining |
-|------------------------------|--------------------------------------------|
-| {} | Empty Set |
-| {E} | Singleton Set |
-| {E,F,...} | Set Enumeration |
-| {x1,...,xn\|P} | Set Comprehension |
-| POW(S) | Power Set |
-| POW1(S) | Set of Non-Empty Subsets |
-| FIN(S) | Set of All Finite Subsets |
-| FIN1(S) | Set of All Non-Empty Finite Subsets |
-| card(S) | Cardinality |
-| S * T | Cartesian Product |
-| S \/ T | Set Union |
-| S /\ T | Set Intersection |
-| S - T | Set Difference |
-| E : S | Element of |
-| E /: S | Not Element of |
-| S <: T | Subset of |
-| S /<: T | Not Subset of |
-| S <<: T | Strict Subset of |
-| S /<<: T | Not Strict Subset of |
-| union(S) | Generalized Union over Sets of Sets |
-| inter(S) | Generalized Intersection over Sets of Sets |
-| UNION(z1,...,zn).(P\|E) | Generalized Union with Predicate |
-| INTER(z1,...,zn).(P\|E) | Generalized Intersection with Predicate |
+| Set expression or predicate | Meaining |
+|-------------------------------|--------------------------------------------|
+| {} | Empty Set |
+| {E} | Singleton Set |
+| {E,F,...} | Set Enumeration |
+| {x1,...,xn\ |P} | Set Comprehension |
+| POW(S) | Power Set |
+| POW1(S) | Set of Non-Empty Subsets |
+| FIN(S) | Set of All Finite Subsets |
+| FIN1(S) | Set of All Non-Empty Finite Subsets |
+| card(S) | Cardinality |
+| S * T | Cartesian Product |
+| S \/ T | Set Union |
+| S /\ T | Set Intersection |
+| S - T | Set Difference |
+| E : S | Element of |
+| E /: S | Not Element of |
+| S <: T | Subset of |
+| S /<: T | Not Subset of |
+| S <<: T | Strict Subset of |
+| S /<<: T | Not Strict Subset of |
+| union(S) | Generalized Union over Sets of Sets |
+| inter(S) | Generalized Intersection over Sets of Sets |
+| UNION(z1,...,zn).(P | E) | Generalized Union with Predicate |
+| INTER(z1,...,zn).(P | E) | Generalized Intersection with Predicate |
Restriction: Set comprehesions, generalized unions and generalized intersections are quantified constructs. The predicate P must be a conjunction where the first n conjuncts must constraint the bounded variables.
The i-th conjunct must constraint xi for each i in {1,...,n}.
@@ -191,8 +191,8 @@ The i-th conjunct must constraint xi for each i in {1,...,n}.
| m / n | Division |
| m ** n | Power |
| m mod n | Remainder of Division |
-| PI(z1,...,zn).(P\|E) | Set product |
-| SIGMA(z1,...,zn).(P\|E) | Set summation |
+| PI(z1,...,zn).(P | E) | Set product |
+| SIGMA(z1,...,zn).(P | E) | Set summation |
| succ(n) | Successor |
| pred(n) | Predecessor |
@@ -205,30 +205,30 @@ The i-th conjunct must constraint xi for each i in {1,...,n}.
### Relations:
-| Relation expression | Meaining |
-|---------------------|-------------------------------------------------------|
-| S <-> T | Set of relation |
-| E \|-> F | Couple |
-| dom(r) | Domain of Relation |
-| range(r) | Range of Relation |
-| id(S) | Identity Relation |
-| S <\| r | Domain Restriction |
-| S <<\| r | Domain Substraction |
-| r \|> S | Range Restriction |
-| r \|>> S | Range Substraction |
-| r~ | Inverse of Relation |
-| r[S] | Relational Image |
-| r1 <+ r2 | Relational Overriding |
-| r1 >< r2 | Direct Product |
-| (r1 ; r2) | Relational Composition |
-| (r1 \|\| r2) | Parallel Product |
-| prj1(S,T) | Projection Function |
-| prj2(S,T) | Projection Function |
-| closure1(r) | Transitive Closure |
-| closure(r) | Transitive Reflxibe Closure |
-| iterate(r,n) | Iteration of r with n |
-| fnc(r) | Translate Relation A <-> B into function A +-> POW(B) |
-| rel(r) | Translate Relation A <-> POW(B) into relation A <-> B |
+| Relation expression | Meaining |
+|----------------------|-------------------------------------------------------|
+| S <-> T | Set of relation |
+| E |-> F | Couple |
+| dom(r) | Domain of Relation |
+| range(r) | Range of Relation |
+| id(S) | Identity Relation |
+| S <| r | Domain Restriction |
+| S <<| r | Domain Substraction |
+| r |> S | Range Restriction |
+| r |>> S | Range Substraction |
+| r~ | Inverse of Relation |
+| r[S] | Relational Image |
+| r1 <+ r2 | Relational Overriding |
+| r1 >< r2 | Direct Product |
+| (r1 ; r2) | Relational Composition |
+| (r1 || r2) | Parallel Product |
+| prj1(S,T) | Projection Function |
+| prj2(S,T) | Projection Function |
+| closure1(r) | Transitive Closure |
+| closure(r) | Transitive Reflxibe Closure |
+| iterate(r,n) | Iteration of r with n |
+| fnc(r) | Translate Relation A <-> B into function A +-> POW(B) |
+| rel(r) | Translate Relation A <-> POW(B) into relation A <-> B |
Restriction: Set of Relation mostly grows up very fast. They are only supported on the right-hand side of a set predicate.
@@ -267,8 +267,8 @@ The i-th conjunct must constraint xi for each i in {1,...,n}.
| front(S) | Front of Sequence |
| tail(S) | Tail of Sequence |
| conc(S) | Concatenation of Sequence of Sequences |
-| s /\|\ n | Take first n elements of sequence |
-| s \\|/ n | Drop first n elements of sequence |
+| s /|\ n | Take first n elements of sequence |
+| s \\|/ n | Drop first n elements of sequence |
The following constructs are not supported for code generation: seq(S), seq1(S), iseq(S), iseq1(S) and perm(S).
They are only allowed in the predicate of constructs for verification such as invariant or precondition.
@@ -313,7 +313,7 @@ Restriction: STRING is a infinite set. It is only supported on the right-hand si
| x :: S | Choice from Set |
| x : (P) | Choice by Predicate |
| x <-- OP(X) | Operation Call and Assignment of Return Value |
-| G \|\| H | Parallel Substitution |
+| G || H | Parallel Substitution |
| G ; H | Sequential Substitution |
| ANY x1,...,xn WHERE P THEN G END | Non Deterministic Choice |
| LET x1,...,xn BE x1=E1 & ... & xn = En IN G END | Let Substitution |
diff --git a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java b/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
index fa3ed53145806e8f8d5d616d0e2c2fc6222d0cfb..eb04bfd2b87217c1d92f78e23efd46f2a5ed2cba 100755
--- a/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
+++ b/src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
@@ -790,10 +790,6 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
return isIncludedMachine;
}
- public boolean isUseBigInteger() {
- return useBigInteger;
- }
-
public InvariantGenerator getInvariantGenerator() {
return invariantGenerator;
}
diff --git a/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
index fb89ccf60fdb22b916d455208510d80a0679c136..e8ebe59136be8f69b52b91bd424c688d3d3d4692 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
@@ -5,7 +5,7 @@ return, short, signed, sizeof, static, static_cast, volatile, struct, switch, te
>>
-machine(forModelChecking, imports, includedMachines, machine, structs, constants_declarations, includes, enums, sets, declarations, initialization, copyConstructor, operations, addition, useBigInteger, getters, transitions, invariant, copy, hash_equal, modelcheck, lambdaFunctions, mainMethod) ::= <<
+machine(forModelChecking, imports, includedMachines, machine, structs, constants_declarations, includes, enums, sets, declarations, initialization, copyConstructor, operations, addition, useBigInteger, getters, transitions, invariant, copy, hash_equal, modelcheck, lambdaFunctions, mainMethod, transitionCachesDeclaration) ::= <<
#include \<iostream>
#include \<string>
<if(forModelChecking)>
@@ -20,6 +20,7 @@ machine(forModelChecking, imports, includedMachines, machine, structs, constants
#include \<boost/asio/post.hpp>
#include \<boost/asio/thread_pool.hpp>
#include \<boost/any.hpp>
+#include \<boost/optional.hpp>
<endif>
<if(useBigInteger)>
#include \<btypes_big_integer/BUtils.hpp>
@@ -78,9 +79,16 @@ class <machine> {
<sets; separator="\n">
<declarations; separator="\n">
+ <if(forModelChecking)>
+ <transitionCachesDeclaration; separator="\n">
+ <endif>
public:
+ <if(forModelChecking)>
+
+ std::string stateAccessedVia;
+ <endif>
<initialization>
@@ -484,18 +492,23 @@ if((<predicate>).booleanValue()) {
>>
transition(noParameters, noPredicate, identifier, subType, operationName, predicate, combination) ::= <<
-<if(noParameters)>bool<else>BSet\<<subType>\><endif> _tr_<operationName>() const {
- <if(noParameters)>
- <if(noPredicate)>
- return true;
- <else>
- return (<predicate>).booleanValue();
- <endif>
- <else>
- BSet\<<subType>\> <identifier> = BSet\<<subType>\>();
- <combination>
- return <identifier>;
- <endif>
+<if(noParameters)>bool<else>BSet\<<subType>\><endif> _tr_<operationName>(bool isCaching) const {
+ if (this->_tr_cache_<operationName> == boost::none){
+ <if(noParameters)>
+ <if(noPredicate)>
+ return true;
+ <else>
+ this->_tr_cache_<operationName> = (<predicate>).booleanValue();
+ return this->_tr_cache_<operationName>.get();
+ <endif>
+ <else>
+ BSet\<<subType>\> <identifier> = BSet\<<subType>\>();
+ <combination>
+ if (isCaching) this->_tr_cache_<operationName> = <identifier>;
+ else return <identifier>;
+ <endif>
+ }
+ return this->_tr_cache_<operationName>.get();
}
>>
@@ -516,9 +529,25 @@ copy_assignment(variable) ::= <<
this-><variable> = <variable>;
>>
-copy(machine, parameters) ::= <<
-<machine> _copy() const {
- return <machine>(<parameters; separator=", ">);
+copy(machine, parameters, operations) ::= <<
+static constexpr unsigned int strHash(const char *s, int off = 0) {
+ return !s[off] ? 5381 : (strHash(s, off+1)*33) ^ s[off];
+}
+
+<machine> _copy(unordered_set\<string> toInvalidate) const {
+ static const char* allTransitions[] = {<operations: {op | "_tr_<op>"}; separator=", ">};
+
+ <machine> result = <machine>(<parameters; separator=", ">);
+
+ for (const auto &item : allTransitions) {
+ if(toInvalidate.find(item) == toInvalidate.end()) {
+ switch(strHash(item)) {
+ <operations: {op | case strHash("_tr_<op>"): result._tr_cache_<op> = this->_tr_cache_<op>; break;}; separator="\n">
+ default: cout \<\< "Transition " \<\< item \<\< " not found!";
+ }
+ }
+ }
+ return result;
}
>>
@@ -993,11 +1022,7 @@ class ModelChecker {
std::unordered_map\<string, std::unordered_set\<string>\> invariantDependency;
std::unordered_map\<string, std::unordered_set\<string>\> guardDependency;
- std::unordered_map\<<machine>, std::unordered_set\<string>, <machine>::Hash, <machine>::HashEqual> dependentInvariant;
- std::unordered_map\<<machine>, std::unordered_set\<string>, <machine>::Hash, <machine>::HashEqual> dependentGuard;
- std::unordered_map\<<machine>, immer::map\<string, boost::any>, <machine>::Hash, <machine>::HashEqual> guardCache;
std::unordered_map\<<machine>, <machine>, <machine>::Hash, <machine>::HashEqual> parents;
- std::unordered_map\<<machine>, string, <machine>::Hash, <machine>::HashEqual> stateAccessedVia;
public:
ModelChecker() {}
@@ -1069,118 +1094,34 @@ model_check(addCachedInfos, nextStates, printResult, checkInvariants, main) ::=
model_check_next_states(machine, transitionsWithCaching, transitionsWithoutCaching) ::= <<
std::unordered_set\<<machine>, <machine>::Hash, <machine>::HashEqual> generateNextStates(const <machine>& state) {
std::unordered_set\<<machine>, <machine>::Hash, <machine>::HashEqual> result = std::unordered_set\<<machine>, <machine>::Hash, <machine>::HashEqual>();
- if(isCaching) {
- immer::map\<string, boost::any> parentsGuard;
- immer::map\<string, boost::any> newCache;
- bool parentsExist = (parents.find(state) != parents.end());
- std::unordered_set\<string> dependentGuardsOfState;
- bool dependentGuardsExist = false;
- {
- std::unique_lock\<std::mutex> lock(guardMutex);
- dependentGuardsExist = (dependentGuard.find(state) != dependentGuard.end());
- if(parentsExist) {
- newCache = guardCache[parents[state]];
- }
- if((dependentGuardsExist)) {
- dependentGuardsOfState = dependentGuard[state];
- }
- }
- boost::any cachedValue;
- bool dependentGuardsBoolean = true;
- <transitionsWithCaching>
- {
- std::unique_lock\<std::mutex> lock(guardMutex);
- guardCache.insert({state, newCache});
- }
- } else {
- <transitionsWithoutCaching>
- }
+ <transitionsWithCaching>
return result;
}
>>
model_check_transition(hasParameters, tupleType, transitionIdentifier, evalTransitions, execTransitions, isCaching) ::= <<
<if(hasParameters)>
-<if(isCaching)>
-BSet\<<tupleType>\> <transitionIdentifier>;
-if(dependentGuardsExist) {
- cachedValue = parentsGuard["<evalTransitions>"];
- dependentGuardsBoolean = (dependentGuardsOfState.find("<evalTransitions>") != dependentGuardsOfState.end());
-}
-if(dependentGuardsExist || dependentGuardsBoolean || !parentsExist) {
- <transitionIdentifier> = state.<evalTransitions>();
-} else {
- <transitionIdentifier> = boost::any_cast\<BSet\<<tupleType>\>>(cachedValue);
-}
-newCache = newCache.set("<evalTransitions>", <transitionIdentifier>);
+BSet\<<tupleType>\> <transitionIdentifier> = state.<evalTransitions>(isCaching);
for(const <tupleType>& param : <transitionIdentifier>) {
<execTransitions>
}
<else>
-BSet\<<tupleType>\> <transitionIdentifier> = state.<evalTransitions>();
-for(const <tupleType>& param : <transitionIdentifier>) {
+if(state.<evalTransitions>(isCaching)) {
<execTransitions>
}
<endif>
-<else>
-<if(isCaching)>
-bool <transitionIdentifier>;
-if(dependentGuardsExist) {
- cachedValue = parentsGuard["<evalTransitions>"];
- dependentGuardsBoolean = (dependentGuardsOfState.find("<evalTransitions>") != dependentGuardsOfState.end());
-}
-if(dependentGuardsExist || dependentGuardsBoolean || parentsExist) {
- <transitionIdentifier> = state.<evalTransitions>();
-} else {
- <transitionIdentifier> = boost::any_cast\<bool>(cachedValue);
-}
-newCache = newCache.set("<evalTransitions>", <transitionIdentifier>);
-if(<transitionIdentifier>) {
- <execTransitions>
-}
-<else>
-if(state.<evalTransitions>()) {
- <execTransitions>
-}
-<endif>
-<endif>
>>
model_check_add_cached_infos(machine) ::= <<
-void addCachedInfos(const std::string& operation, const <machine>& state, const <machine>& copiedState) {
- if(isCaching) {
- std::unique_lock\<std::mutex> lock(guardMutex);
- if(dependentInvariant.find(copiedState) == dependentInvariant.end()) {
- dependentInvariant.insert({copiedState, invariantDependency[operation]});
- }
- if(dependentGuard.find(copiedState) == dependentGuard.end()) {
- dependentGuard.insert({copiedState, guardDependency[operation]});
- }
- if(stateAccessedVia.find(copiedState) == stateAccessedVia.end()) {
- stateAccessedVia.insert({copiedState, operation});
- }
- if(parents.find(copiedState) == parents.end()) {
- parents.insert({copiedState, state});
- }
- } else {
- std::unique_lock\<std::mutex> lock(guardMutex);
- if(stateAccessedVia.find(copiedState) == stateAccessedVia.end()) {
- stateAccessedVia.insert({copiedState, operation});
- }
- if(parents.find(copiedState) == parents.end()) {
- parents.insert({copiedState, state});
- }
- }
-}
>>
model_check_transition_body(machine, operation, hasParameters, readParameters, parameters, isCaching) ::= <<
<if(hasParameters)>
<readParameters>
<endif>
-<machine> copiedState = state._copy();
+<machine> copiedState = state._copy(guardDependency["<operation>"]);
copiedState.<operation>(<parameters; separator=", ">);
-addCachedInfos(std::string("<operation>"), state, copiedState);
+copiedState.stateAccessedVia = "<operation>";
result.insert(copiedState);
transitions += 1;
>>
@@ -1199,6 +1140,8 @@ 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];
<invariantViolated; separator="\n">
return false;
}
@@ -1206,7 +1149,6 @@ bool invariantViolated(const <machine>& state) {
model_check_invariant(invariant) ::= <<
if(isCaching) {
- std::unordered_set\<string> dependentInvariantsOfState = dependentInvariant[state];
if(dependentInvariantsOfState.find("<invariant>") == dependentInvariantsOfState.end()) {
if(!state.<invariant>()) {
cout \<\< "INVARIANT CONJUNCT VIOLATED: <invariant>" \<\< "\n";
@@ -1245,7 +1187,7 @@ void printResult() {
stringStream \<\< counterExampleState;
trace.insert(0, stringStream.str());
trace.insert(0, "\n");
- trace.insert(0, stateAccessedVia[counterExampleState]);
+ trace.insert(0, counterExampleState.stateAccessedVia);
trace.insert(0, "\n\n");
counterExampleState = parents[counterExampleState];
}
@@ -1294,6 +1236,7 @@ void modelCheckSingleThreaded() {
for(auto& nextState : nextStates) {
if(states.find(nextState) == states.end()) {
states.insert(nextState);
+ parents.insert({nextState, state});
unvisitedStates.push_back(nextState);
if(states.size() % 50000 == 0) {
cout \<\< "VISITED STATES: " \<\< states.size() \<\< "\n";
@@ -1347,6 +1290,7 @@ void modelCheckMultiThreaded(boost::asio::thread_pool& workers) {
std::unique_lock\<std::mutex> lock(mutex);
if(states.find(nextState) == states.end()) {
states.insert(nextState);
+ parents.insert({nextState, state});
unvisitedStates.push_back(nextState); // TODO: sync ?
if(isDebug && states.size() % 50000 == 0) {
cout \<\< "VISITED STATES: " \<\< states.size() \<\< "\n";
@@ -1389,7 +1333,7 @@ void modelCheckMultiThreaded(boost::asio::thread_pool& workers) {
{
std::unique_lock\<std::mutex> lock(waitMutex);
- if (unvisitedStates.empty() && possibleQueueChanges > 0) {
+ while (unvisitedStates.empty() && possibleQueueChanges > 0) {
waitCV.wait(lock, [&] {
return waitFlag == false;
});
@@ -1402,8 +1346,8 @@ void modelCheckMultiThreaded(boost::asio::thread_pool& workers) {
void initCache(<machine>& machine) {
<invariantDependency; separator="\n">
+ invariantDependency.insert({"", {}});
<guardDependency; separator="\n">
- dependentInvariant.insert({machine, std::unordered_set\<string>()});
}
>>
@@ -1472,4 +1416,5 @@ include_initialization() ::= <<
>>
transition_cache_declaration(type, identifier, operationHasParams) ::= <<
+mutable boost::optional\<<if(operationHasParams)>BSet\<<type>\><else>bool<endif>\> _tr_cache_<identifier>;
>>