Skip to content
Snippets Groups Projects
Commit 167e8dfa authored by Cookiebowser's avatar Cookiebowser
Browse files

optimized c++ Template (MC)

parent 8a60d560
No related branches found
No related tags found
1 merge request!28Rust support
Show whitespace changes
Inline Side-by-side
README.md
+ 54
− 54
View file @ 167e8dfa
......@@ -137,7 +137,7 @@ 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 |
......@@ -159,8 +159,8 @@ P is a conjunction of n conjuncts where the i-th conjunct must constraint xi for
| 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 |
| UNION(z1,...,zn).(P &#124; E) | Generalized Union with Predicate |
| INTER(z1,...,zn).(P &#124; 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 &#124; E) | Set product |
| SIGMA(z1,...,zn).(P &#124; E) | Set summation |
| succ(n) | Successor |
| pred(n) | Predecessor |
......@@ -206,22 +206,22 @@ 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 |
| E &#124;-> 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 |
| S <&#124; r | Domain Restriction |
| S <<&#124; r | Domain Substraction |
| r &#124;> S | Range Restriction |
| r &#124;>> 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 |
| (r1 &#124;&#124; r2) | Parallel Product |
| prj1(S,T) | Projection Function |
| prj2(S,T) | Projection Function |
| closure1(r) | Transitive Closure |
......@@ -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 /&#124;\ n | Take first n elements of sequence |
| s \\&#124;/ 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 &#124;&#124; 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 |
......
src/main/java/de/hhu/stups/codegenerator/generators/MachineGenerator.java
+ 0
− 4
View file @ 167e8dfa
......@@ -790,10 +790,6 @@ public class MachineGenerator implements AbstractVisitor<String, Void> {
return isIncludedMachine;
}
public boolean isUseBigInteger() {
return useBigInteger;
}
public InvariantGenerator getInvariantGenerator() {
return invariantGenerator;
}
......
src/main/resources/de/hhu/stups/codegenerator/CppTemplate.stg
+ 58
− 113
View file @ 167e8dfa
......@@ -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,19 +492,24 @@ if((<predicate>).booleanValue()) {
>>
transition(noParameters, noPredicate, identifier, subType, operationName, predicate, combination) ::= <<
<if(noParameters)>bool<else>BSet\<<subType>\><endif> _tr_<operationName>() const {
<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>
return (<predicate>).booleanValue();
this->_tr_cache_<operationName> = (<predicate>).booleanValue();
return this->_tr_cache_<operationName>.get();
<endif>
<else>
BSet\<<subType>\> <identifier> = BSet\<<subType>\>();
<combination>
return <identifier>;
if (isCaching) this->_tr_cache_<operationName> = <identifier>;
else return <identifier>;
<endif>
}
return this->_tr_cache_<operationName>.get();
}
>>
invariant(invariantFunction, iterationConstruct, predicate) ::= <<
......@@ -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>
}
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>);
for(const <tupleType>& param : <transitionIdentifier>) {
<execTransitions>
}
<else>
BSet\<<tupleType>\> <transitionIdentifier> = state.<evalTransitions>();
BSet\<<tupleType>\> <transitionIdentifier> = state.<evalTransitions>(isCaching);
for(const <tupleType>& param : <transitionIdentifier>) {
<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>()) {
if(state.<evalTransitions>(isCaching)) {
<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>;
>>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment