Commit a97e99ae authored by Jonathan Shahen's avatar Jonathan Shahen

Adding main class for quick conversion; chaning unused statevariables to...

Adding main class for quick conversion; chaning unused statevariables to staying FALSE (might increase speed, might not)
parent a7c6cc82
......@@ -40,6 +40,11 @@ public class ConverterInstance {
public MohawkTiming timing = new MohawkTiming();
public FileExtensions fileExt = new FileExtensions();
public static void main(String[] args) {
ConverterInstance ci = new ConverterInstance();
ci.run(args);
}
private CommandLine init(String[] args) throws Exception {
Options options = new Options();
setupOptions(options);
......
......@@ -11,6 +11,15 @@ numtimeslots := <numTimeSlots>;
LTLSPEC G !(<goalRoles:{r|u[1]<r.string> = TRUE}; separator=" & ">)
VAR
user : 1 .. numusers;
admin: 1 .. numusers;
u : array 1..numusers of
array 1..numroles of
array 1..numtimeslots of boolean;
e : array 1..numroles of
array 1..numtimeslots of boolean;
rule : {
-- CanAssign
<caruleslist>
......@@ -21,14 +30,6 @@ rule : {
-- CanDisable
<cdruleslist>
};
user : 1 .. numusers;
admin: 1 .. numusers;
u : array 1..numusers of
array 1..numroles of
array 1..numtimeslots of boolean;
e : array 1..numroles of
array 1..numtimeslots of boolean;
ASSIGN
......@@ -43,7 +44,7 @@ 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>]) := FALSE; --u[<u>][<r.role>][<ts.timeslot>];
<endif>
}; separator="\n">
<else>-- Skipping <r.role>
......@@ -61,7 +62,7 @@ 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(e[<r.role>][<ts.timeslot>]) := e[<r.role>][<ts.timeslot>];
<else>next(e[<r.role>][<ts.timeslot>]) := FALSE; --e[<r.role>][<ts.timeslot>];
<endif>
}; separator="\n">
<else>-- Skipping <r.role>
......
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