Skip to content
Snippets Groups Projects
Commit 17fd0f3e authored by Cookiebowser's avatar Cookiebowser
Browse files

adjusted rust template to MC-generator changes

parent a7c50c89
No related branches found
No related tags found
1 merge request!28Rust support
......@@ -788,12 +788,12 @@ if state.<evalTransitions>(isCaching) {
<endif>
>>
model_check_invariants(machine, checkInvariants, invariants) ::= <<
model_check_invariants(machine, invariantViolated, invariants) ::= <<
//model_check_invariants
pub fn checkInvariants(state: &<machine>, last_op: &'static str, isCaching: bool) -> bool {
if isCaching {
let dependent_invariants_of_state = Self::get_invariant_dependencies(last_op);
<checkInvariants; separator="\n">
<invariantViolated; separator="\n">
return true;
}
return !(<invariants:{inv | !state.<inv>()}; separator=" || ">);
......@@ -1089,3 +1089,15 @@ if (<predicate>).booleanValue() {
}
<endif>
>>
model_check_main_method() ::= <<>>
modelchecker(main, invariantViolated, printResult, nextStates) ::= <<
<nextStates>
<invariantViolated>
<printResult>
<main>
>>
model_check_add_cached_infos() ::= <<>>
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment