Commit cdd36ea1 authored by Jonathan Shahen's avatar Jonathan Shahen

Forgot to add this last time; separated out the different version of SMV...

Forgot to add this last time; separated out the different version of SMV templates; required for the build script to work
parent 741ac8b5
......@@ -25,7 +25,7 @@ ASSIGN
$ua; separator=";\n"$;
-- This section will contain state transition rules
$transitions; separator= "\n-- Another user \n" $
$transitions; separator= "\n\n\n-- ----------------------------------\n-- Another user \n\n\n" $
-- LTLSPEC: "G p" means that a certain condition p holds in all future time instants
LTLSPEC G ($user$[$roleindex$]=$falseWord$)
\ No newline at end of file
-- This NuSMV specification was automatically generated by Mohawk 2.0
-- Stats
-- Number of role without rules: <roleWithoutRules>
-- Number of role with rules: <roleWithRules>
-- Ratio without / with: <roleWithoutWithRatio>
-- Ratio without / total: <roleWithoutTotalRatio>
MODULE main
VAR
-- This section will contain state variables. For each user, we will have
-- an array.
<userarrays; separator=";\n">;
-- This section will contain enumerations for users and actions
act : {ADD, REMOVE};
user : {<users; separator=",">};
admin : {<admin; separator=",">};
role : <role>;
ASSIGN
-- Assigning UA
<ua; separator=";\n">;
-- This section will contain state transition rules
<transitions; separator= "\n\n\n-- ----------------------------------\n-- Another user \n\n\n">
-- LTLSPEC: "G p" means that a certain condition p holds in all future time instants
LTLSPEC G (<user>[<roleindex>]=<falseWord>)
\ No newline at end of file
-- $rolename$
next($roleindex1$) :=
case
$transition; separator=";\n" $
$trueWord$ : $roleindex2$;
esac;
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment