Commit d7a2d4ac authored by Jonathan Shahen's avatar Jonathan Shahen

HOTFIX: fixing compilation error - got a working positive, need to test...

HOTFIX: fixing compilation error - got a working positive, need to test negatives and more positives
parent b06818a8
......@@ -88,9 +88,11 @@ public class ConvertToNuSMV extends ConvertTo {
st.add("goalRoles", RoleTimeSlot.grabAll(m.query._roles, m.query._timeslot, m.timeIntervalHelper,
m.roleHelper));
st.add("caruleslist", stringList("CA", caRuleCount));
st.add("crruleslist", stringList("CR", crRuleCount));
st.add("ceruleslist", stringList("CE", ceRuleCount));
st.add("caruleslist", stringList("CA", caRuleCount)
+ ((caRuleCount > 0 & (crRuleCount > 0 | ceRuleCount > 0 | cdRuleCount > 0)) ? "," : ""));
st.add("crruleslist", stringList("CR", crRuleCount)
+ ((crRuleCount > 0 & (ceRuleCount > 0 | cdRuleCount > 0)) ? "," : ""));
st.add("ceruleslist", stringList("CE", ceRuleCount) + ((ceRuleCount > 0 & (cdRuleCount > 0)) ? "," : ""));
st.add("cdruleslist", stringList("CD", cdRuleCount));
st.add("users", users);
......
......@@ -8,7 +8,7 @@ numtimeslots := <numTimeSlots>;
-- LTLSPEC: "G p" means that a certain condition p holds in all future time instants
-- <queryStr>
LTLSPEC G !(<goalRoles:{r|U1<r.string> = TRUE}; separator=" & ">)
LTLSPEC G !(<goalRoles:{r|u[1]<r.string> = TRUE}; separator=" & ">)
VAR
rule : {
......@@ -24,10 +24,10 @@ rule : {
user : 1 .. numusers;
admin: 1 .. numusers;
U : array 1..numusers of
u : array 1..numusers of
array 1..numroles of
array 1..numtimeslots of boolean;
RE : array 1..numroles of
e : array 1..numroles of
array 1..numtimeslots of boolean;
ASSIGN
......@@ -39,11 +39,11 @@ ASSIGN
-- User <u>, Role <r.role> Assign/Revoke
<r.timeslots:{ts|
<if(ts.cases)>
next(U[<u>][<r.role>][<ts.timeslot>]) := case
<ts.cases:{c|<\t>user=<u> & <c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>}; separator="\n">
<\t>TRUE : U[<u>][<r.role>][<ts.timeslot>];
next(u[<u>][<r.role>][<ts.timeslot>]) := case
<ts.cases:{c|<\t>user=<u> & <c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>;}; separator="\n">
<\t>TRUE : u[<u>][<r.role>][<ts.timeslot>];
esac;
<else>next(U[<u>][<r.role>][<ts.timeslot>]) := U[<u>][<r.role>][<ts.timeslot>];
<else>next(u[<u>][<r.role>][<ts.timeslot>]) := u[<u>][<r.role>][<ts.timeslot>];
<endif>
}; separator="\n">
<else>-- Skipping <r.role>
......@@ -57,11 +57,11 @@ esac;
-- Role <r.role> Enable/Disable
<r.timeslots:{ts|
<if(ts.cases)>
next(RE[<r.role>][<ts.timeslot>]) := case
<ts.cases:{c|<\t><c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>}; separator="\n">
<\t>TRUE : RE[<r.role>][<ts.timeslot>];
next(e[<r.role>][<ts.timeslot>]) := case
<ts.cases:{c|<\t><c.condition> : <if(c.trueResult)>TRUE<else>FALSE<endif>;}; separator="\n">
<\t>TRUE : e[<r.role>][<ts.timeslot>];
esac;
<else>next(RE[<r.role>][<ts.timeslot>]) := RE[<r.role>][<ts.timeslot>];
<else>next(e[<r.role>][<ts.timeslot>]) := e[<r.role>][<ts.timeslot>];
<endif>
}; separator="\n">
<else>-- Skipping <r.role>
......@@ -77,13 +77,13 @@ VAR
<users:{u|<roleTimeslots:{rt|U<u><rt.string> : boolean;}; separator=" ">}; separator="\n">
-- <numRolesEnabled> RoleEnabled
<enabledRoles:{rt|RE<rt.string> : boolean;}; separator=" ">
<enabledRoles:{rt|e<rt.string> : boolean;}; separator=" ">
------------------------------------------------------------
!>
ASSIGN
-- Disabling User Role Assignments
<users:{u|<roleTimeslots:{rt|init(U[<u>]<rt.string>) := FALSE;}; separator=" ">}; separator="\n">
<users:{u|<roleTimeslots:{rt|init(u[<u>]<rt.string>) := FALSE;}; separator=" ">}; separator="\n">
-- Disabling Roles
<enabledRoles:{rt|init(RE<rt.string>) := FALSE;}; separator=" ">
\ No newline at end of file
<enabledRoles:{rt|init(e<rt.string>) := FALSE;}; separator=" ">
\ 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