Commit b4f583a8 authored by Jonathan Shahen's avatar Jonathan Shahen

Started work on Always On Rules

Finished work on Query conversion

Added some testcases to answer some fundamental questions about the other programs
parent 444d9788
Query: t0, role1
Expected: REACHABLE
CanAssign {
<TRUE, t1, TRUE, t0, role1>
<TRUE, t1, TRUE, t0, role2>
}
CanRevoke {}
CanEnable {}
CanDisable {}
\ No newline at end of file
Query: t0, [role1]
Expected: REACHABLE
CanAssign {
<TRUE, t2, TRUE, [t1], role1>
<role1, t1, TRUE, [t0], role2>
}
CanRevoke {}
CanEnable {}
CanDisable {}
\ No newline at end of file
......@@ -17,6 +17,7 @@ import mohawk.converter.logging.MohawkCSVFileFormatter;
import mohawk.converter.logging.MohawkConsoleFormatter;
import mohawk.converter.logging.MohawkTiming;
import mohawk.converter.to.asaptime.ConvertToASAPTimeNSA;
import mohawk.converter.to.asaptime.ConvertToASAPTimeSA;
import mohawk.converter.to.mohawk.ConvertToMohawk;
import mohawk.converter.to.tred.ConvertToTRule;
import mohawk.global.FileExtensions;
......@@ -118,20 +119,39 @@ public class ConverterInstance {
logger.info("[CONVERTING] Converting to ASAPTime NSA...");
/* Timing */timing.startTimer("convertToASAPTimeNSA (" + i + ")");
ConvertToASAPTimeNSA toRanise = new ConvertToASAPTimeNSA();
toRanise.convert(m, specFile, true);
ConvertToASAPTimeNSA toASAPTimeNSA = new ConvertToASAPTimeNSA();
toASAPTimeNSA.convert(m, specFile, true);
if (toRanise.lastError == null) {
logger.info("[SUCCESS] Successfully converted to Ranise's Input Format");
if (toASAPTimeNSA.lastError == null) {
logger.info("[SUCCESS] Successfully converted to ASAPTimeNSA's Input Format");
} else {
logger.warning("[FAILURE] Failed to convert to Raines's Input Format; Error code "
+ toRanise.lastError);
logger.warning("[FAILURE] Failed to convert to ASAPTimeNSA's Input Format; Error code "
+ toASAPTimeNSA.lastError);
}
/* Timing */timing.stopTimer("convertToRanise (" + i + ")");
/* Timing */timing.stopTimer("convertToASAPTimeNSA (" + i + ")");
logger.info("[CONVERTING] ...Done Converting to ASAPTime NSA");
}
if (cmd.hasOption(OptionString.TO_ASAPTIME_SA.toString())
|| cmd.hasOption(OptionString.TO_ALL.toString())) {
logger.info("[CONVERTING] Converting to ASAPTime SA...");
/* Timing */timing.startTimer("convertToASAPTimeSA (" + i + ")");
ConvertToASAPTimeSA toASAPTimeSA = new ConvertToASAPTimeSA();
toASAPTimeSA.convert(m, specFile, true);
if (toASAPTimeSA.lastError == null) {
logger.info("[SUCCESS] Successfully converted to ASAPTimeSA's Input Format");
} else {
logger.warning("[FAILURE] Failed to convert to ASAPTimeSA's Input Format; Error code "
+ toASAPTimeSA.lastError);
}
/* Timing */timing.stopTimer("convertToASAPTimeSA (" + i + ")");
logger.info("[CONVERTING] ...Done Converting to ASAPTime SA");
}
if (cmd.hasOption(OptionString.TO_TRULE.toString()) || cmd.hasOption(OptionString.TO_ALL.toString())) {
logger.info("[CONVERTING] Converting to TRule...");
/* Timing */timing.startTimer("convertToTRule (" + i + ")");
......
......@@ -9,6 +9,7 @@ import java.util.logging.Logger;
import mohawk.converter.generated.MohawkTARBACParser;
import mohawk.converter.logging.MohawkConsoleFormatter;
import mohawk.converter.to.asaptime.ConvertToASAPTimeNSA;
import mohawk.converter.to.asaptime.ConvertToASAPTimeSA;
import mohawk.global.pieces.MohawkT;
import org.junit.Before;
......@@ -31,7 +32,7 @@ public class ConvertToASAPTimeTests {
}
@Test
public void printOut() throws IOException {
public void printOutNSA() throws IOException {
String file = "positive1.spec";
error.errorFound = false;
......@@ -47,6 +48,23 @@ public class ConvertToASAPTimeTests {
}
@Test
public void printOutSA() throws IOException {
String file = "positive1.spec";
error.errorFound = false;
MohawkTARBACParser parser = loadfile(file);
MohawkT m = parser.mohawkT;
ConvertToASAPTimeSA converter = new ConvertToASAPTimeSA();
String convertedStr = converter.convert(m, null, false);
System.out.println("Printing Out: " + file);
System.out.println(convertedStr + "\n\n");
}
private MohawkTARBACParser loadfile(String file) throws IOException {
FileInputStream fis = new FileInputStream(folderbase + file);
......
package mohawk.converter.testing;
import java.io.FileInputStream;
import java.io.IOException;
import java.util.logging.ConsoleHandler;
import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.converter.generated.MohawkTARBACParser;
import mohawk.converter.logging.MohawkConsoleFormatter;
import mohawk.converter.to.tred.ConvertToTRole;
import mohawk.global.pieces.MohawkT;
import org.junit.Before;
import org.junit.Test;
public class ConvertToTRoleTests {
public static final Logger logger = Logger.getLogger("mohawk-converter");
public String folderbase = "data/regressiontests/";
public BooleanErrorListener error = new BooleanErrorListener();
@Before
public void setup() {
System.out.println("sadasdasdasdsadsadsaasd");
logger.setLevel(Level.FINE);
ConsoleHandler consoleHandler = new ConsoleHandler();
consoleHandler.setFormatter(new MohawkConsoleFormatter());
consoleHandler.setLevel(Level.FINE);
logger.addHandler(consoleHandler);
}
@Test
public void printOut() throws IOException {
String file = "positive1.spec";
error.errorFound = false;
MohawkTARBACParser parser = loadfile(file);
MohawkT m = parser.mohawkT;
ConvertToTRole converter = new ConvertToTRole();
String convertedStr = converter.convert(m, null, false);
System.out.println("Printing Out: " + file);
System.out.println(convertedStr + "\n\n");
}
private MohawkTARBACParser loadfile(String file) throws IOException {
FileInputStream fis = new FileInputStream(folderbase + file);
return ConverterRegressionTests.runParser(fis, error);
}
}
......@@ -38,4 +38,8 @@ public class ConvertTo {
return new String(encoded, encoding);
}
public static String readFile(URL url) throws IOException, URISyntaxException {
return readFile(url, Charset.defaultCharset());
}
}
<! Conversion to ASAPTime's SA Input Format !>
<! Conversion to ASAPTime SA Input Format !>
<! !>
CONFIG <numRoles> <numTimeslots>
GOAL <goalRole> <goalTimeslot>
<! !>
<! can_revoke t3 , true ; t5 , 14 !>
<rules:{r|<r.ruleType> <r.adminTime> , <if(r.precondition)><r.precondition; separator=" & "><else>true<endif> ; <r.roleTime> , <r.role><\n>}>
\ No newline at end of file
<rules_sa:{r|<r.ruleType> t<r.adminTime> , <if(r.precondition)><r.precondition; separator=" & "><else>true<endif> ; t<r.roleTime> , <r.role><\n>}>
\ No newline at end of file
......@@ -87,6 +87,8 @@ public class ConvertToASAPTimeNSA extends ConvertTo {
* new Rule such that only someone who has reached the Goal Roles in the original Query can assign this new Goal
* Role and thus make the system REACHABLE.
*
* From the paper, this is the reduction (1) Query, Type 1
*
* WARNING: if this function has to create a new role then it will call roleHelper.setupSortedRoles();
*
* @param query
......
......@@ -5,31 +5,68 @@ import java.io.PrintWriter;
import java.io.StringWriter;
import java.nio.charset.Charset;
import java.nio.file.Files;
import java.util.ArrayList;
import java.util.SortedSet;
import java.util.TreeSet;
import java.util.logging.Logger;
import mohawk.converter.to.ConvertTo;
import mohawk.global.helper.RoleHelper;
import mohawk.global.helper.TimeIntervalHelper;
import mohawk.global.pieces.MohawkT;
import mohawk.global.pieces.Query;
import mohawk.global.pieces.Role;
import mohawk.global.pieces.Rule;
import mohawk.global.pieces.TimeSlot;
import mohawk.global.pieces.reduced.query.ASAPTimeSA_Query;
import mohawk.global.pieces.reduced.rules.ASAPTimeSA_Rule;
import org.stringtemplate.v4.ST;
public class ConvertToASAPTimeSA extends ConvertTo {
public static final Logger logger = Logger.getLogger("mohawk-converter");
public static final Logger logger = Logger.getGlobal();
@Override
public String convert(MohawkT m, File f, Boolean writeToFile) {
public String convert(MohawkT m, File file, Boolean writeToFile) {
try {
String template = ConvertTo.readFile(this.getClass().getResource("ASAPTimeSATemplate.st"),
Charset.defaultCharset());
ST st = new ST(template);
ArrayList<ASAPTimeSA_Rule> newRules = new ArrayList<ASAPTimeSA_Rule>();
ArrayList<Rule> workableRules = new ArrayList<Rule>();
workableRules = m.roleHelper.removeEnableDisableRules(m.getAllRules());
// Reduce Roles to Integers
m.roleHelper.allowZeroRole = false; // roles start from 1 NOT 0!
m.roleHelper.setupSortedRoles();
// Reduce TimeIntervals to Timeslots
m.timeIntervalHelper.allowZeroTimeslot = false; // time-slots start from t1 NOT t0!
m.timeIntervalHelper.reduceToTimeslots();
// Convert Query to Reduced ASAPTime SA Query and add any extra rules as needed
ASAPTimeSA_Query query = toASAPTimeSA_Query(m.query, workableRules, m.roleHelper, m.timeIntervalHelper);
workableRules = m.roleHelper.alwaysOnRules(workableRules, m.timeIntervalHelper);
// Convert Rules into Reduced ASAPTime SA Rules
for (Rule r : workableRules) {
newRules.addAll(toASAPTimeSA_Rules(r, m.roleHelper, m.timeIntervalHelper));
}
logger.fine("Rules: " + m.getAllRules());
logger.fine("Reduced Rules: " + newRules);
st.add("numRoles", m.roleHelper.size());
st.add("numTimeslots", m.timeIntervalHelper.size());
st.add("goalRole", null);
st.add("goalTimeslot", null);
st.add("numTimeslots", m.timeIntervalHelper.sizeReduced());
st.add("goalRole", query.goalRole);
st.add("goalTimeslot", query.goalTimeslot);
st.add("rules_sa", newRules);
convertedStr = st.render();
if (writeToFile) {
File convertedFile = new File(f.getAbsolutePath() + getFileExtenstion());
File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
if (!convertedFile.exists()) {
convertedFile.createNewFile();
......@@ -49,6 +86,99 @@ public class ConvertToASAPTimeSA extends ConvertTo {
return convertedStr;
}
/**
* Directly converts the Query's timeslot to the reduced timeslot and then it copies the Goal Role is there is only
* 1. If there is more than 1 Goal Role in the Query then it will create a new Goal Role that is unique and create a
* new Rule such that only someone who has reached the Goal Roles in the original Query can assign this new Goal
* Role and thus make the system REACHABLE.
*
* From the paper, this is the reduction (1) Query, Type 1
*
* WARNING: if this function has to create a new role then it will call roleHelper.addUniqueRole();
*
* @param query
* @param rules
* @param roleHelper
* @param timeIntervalHelper
* @return
*/
public ASAPTimeSA_Query toASAPTimeSA_Query(Query query, ArrayList<Rule> rules, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
ASAPTimeSA_Query q = new ASAPTimeSA_Query();
// Set the Goal Timeslot
SortedSet<Integer> goalTimeslots = timeIntervalHelper.indexOfReduced(query._timeslot);
assert (goalTimeslots.size() == 1) : "The reduced query must have only one timeslot";
q.goalTimeslot = goalTimeslots.first();
// Set the Goal Role
assert (query._roles.size() > 0) : "The query must have atleast one Goal Role";
if (query._roles.size() == 1) {
q.goalRole = roleHelper.indexOf(query._roles.get(0));
} else {
// Create a new role to act as the Goal Role
Role newGoalRole = roleHelper.addUniqueRole("goalRole");
Rule newRule = new Rule(query, newGoalRole);
rules.add(newRule);
q.goalRole = roleHelper.indexOf(newGoalRole);
}
return q;
}
/**
*
* @param rule
* @param roleHelper
* @param timeIntervalHelper
* @return
*/
public ArrayList<ASAPTimeSA_Rule> toASAPTimeSA_Rules(Rule rule, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
ArrayList<ASAPTimeSA_Rule> rules = new ArrayList<ASAPTimeSA_Rule>();
SortedSet<Integer> adminInterval = timeIntervalHelper.indexOfReduced(rule._adminTimeInterval);
SortedSet<Integer> roleSchedule = new TreeSet<Integer>();
ArrayList<Integer> precondition = new ArrayList<Integer>();
// Convert RoleSchedule to the New Timeslots
for (TimeSlot ts : rule._roleSchedule) {
roleSchedule.addAll(timeIntervalHelper.indexOfReduced(ts));
}
// Convert Preconditions to the Role Indexes
for (Role r : rule._preconditions) {
precondition.add(roleHelper.indexOf(r));
}
logger.fine("Timeslots: " + timeIntervalHelper._timeIntervals);
logger.fine("Reduced Timeslots: " + timeIntervalHelper._reducedTimeIntervals);
logger.fine("Admin Interval: " + adminInterval);
logger.fine("Role Schedule: " + roleSchedule);
ASAPTimeSA_Rule rule_t;
for (Integer adminTimeslot : adminInterval) {
for (Integer roleTimeslot : roleSchedule) {
rule_t = new ASAPTimeSA_Rule();
rule_t.ruleType = rule._type.toRanise();
if (!rule._adminRole.isAllRoles()) { throw new IllegalArgumentException(
"Rule contains a Admin Role that isn't TRUE!"); }
rule_t.adminTime = adminTimeslot;
rule_t.role = roleHelper.indexOf(rule._role);
rule_t.precondition = precondition;
rule_t.roleTime = roleTimeslot;
logger.fine("Adding rule to rules");
rules.add(rule_t);
}
}
return rules;
}
@Override
public String getFileExtenstion() {
return fileExt.ASAPTime_SA;
......
......@@ -3,12 +3,21 @@ package mohawk.converter.to.mohawk;
import java.io.File;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.nio.charset.Charset;
import java.nio.file.Files;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.logging.Logger;
import mohawk.converter.to.ConvertTo;
import mohawk.global.helper.RoleHelper;
import mohawk.global.helper.TimeIntervalHelper;
import mohawk.global.pieces.MohawkT;
import mohawk.global.pieces.Query;
import mohawk.global.pieces.Role;
import mohawk.global.pieces.Rule;
import mohawk.global.pieces.RuleType;
import mohawk.global.pieces.TimeSlot;
import mohawk.global.pieces.reduced.query.Mohawk_Query;
import org.stringtemplate.v4.ST;
......@@ -18,13 +27,31 @@ public class ConvertToMohawk extends ConvertTo {
@Override
public String convert(MohawkT m, File f, Boolean writeToFile) {
try {
String template = ConvertTo.readFile(this.getClass().getResource("raniseTemplate.st"),
Charset.defaultCharset());
String template = ConvertTo.readFile(this.getClass().getResource("mohawkTemplate.st"));
ArrayList<Rule> workableRules = new ArrayList<Rule>();
workableRules = m.roleHelper.removeEnableDisableRules(m.getAllRules());
// Reduce Roles to Integers
m.roleHelper.allowZeroRole = false; // roles start from 1 NOT 0!
m.roleHelper.setupSortedRoles();
// Reduce TimeIntervals to Timeslots
m.timeIntervalHelper.allowZeroTimeslot = false; // time-slots start from t1 NOT t0!
m.timeIntervalHelper.reduceToTimeslots();
// Convert Query to Reduced ASAPTime SA Query and add any extra rules as needed
Mohawk_Query query = toMohawk_Query(m.query, workableRules, m.roleHelper, m.timeIntervalHelper);
query.finalize(m.roleHelper);
ST st = new ST(template);
st.add("numRoles", m.roleHelper.size());
st.add("numTimeslots", null);
st.add("goalRole", null);
st.add("goalTimeslot", null);
st.add("roles", m.roleHelper._roles);
st.add("users", null);
st.add("ua", null);
st.add("cr", null);
st.add("ca", null);
st.add("adminusers", null);
st.add("spec", null);
convertedStr = st.render();
......@@ -49,6 +76,30 @@ public class ConvertToMohawk extends ConvertTo {
return convertedStr;
}
private Mohawk_Query toMohawk_Query(Query query, ArrayList<Rule> rules, RoleHelper roleHelper,
TimeIntervalHelper timeIntervalHelper) {
// Checking Conditions
assert (query._roles.size() > 0) : "The query must have atleast one Goal Role";
Role newGoalRole = roleHelper.addUniqueRole("goalRole");
Mohawk_Query q = new Mohawk_Query(newGoalRole);
Rule newRule = new Rule();
newRule._type = RuleType.ASSIGN;
newRule._adminRole = Role.allRoles();
newRule._adminTimeInterval = timeIntervalHelper.getAllTimeInterval();
newRule._preconditions.addAll(query._roles);
newRule._roleSchedule = new ArrayList<TimeSlot>(Arrays.asList(query._timeslot));
newRule._role = newGoalRole;
rules.add(newRule);
return q;
}
public Integer removeTemporality(Integer roleIndex, Integer timeslotIndex, Integer numberOfRoles) {
return numberOfRoles * (timeslotIndex - 1) + roleIndex;
}
@Override
public String getFileExtenstion() {
return fileExt.Mohawk;
......
Roles $roles; separator=" "$;
Users $users; separator=" "$;
UA $ua; separator=" "$;
CR $cr; separator=" "$;
CA $ca; separator=" "$;
ADMIN $adminusers; separator=" "$;
SPEC $spec; separator=" "$;
package mohawk.converter.to.tred;
import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.nio.charset.Charset;
import java.nio.file.Files;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.SortedSet;
import java.util.TreeSet;
import java.util.logging.Logger;
import mohawk.converter.to.ConvertTo;
import mohawk.global.helper.RoleHelper;
import mohawk.global.helper.TimeIntervalHelper;
import mohawk.global.pieces.MohawkT;
import mohawk.global.pieces.Query;
import mohawk.global.pieces.Role;
import mohawk.global.pieces.Rule;
import mohawk.global.pieces.reduced.rules.TRedRule_Rule;
import mohawk.global.pieces.RuleType;
import mohawk.global.pieces.TimeSlot;
import mohawk.global.pieces.reduced.query.TRole_Query;
import mohawk.global.pieces.reduced.rules.TRole_Rule;
import org.stringtemplate.v4.ST;
public class ConvertToTRole extends ConvertTo {
public static final Logger logger = Logger.getLogger("mohawk-converter");
public static final Logger logger = Logger.getGlobal();
@Override
public String convert(MohawkT m, File f, Boolean writeToFile) {
public String convert(MohawkT m, File file, Boolean writeToFile) {
try {
String template = ConvertTo.readFile(this.getClass().getResource("uzunTemplate.st"),
Charset.defaultCharset());
ST st = new ST(template);
st.add("numRoles", m.roleHelper.size());
st.add("numTimeSlots", m.timeIntervalHelper.getNextTimeSlot());
st.add("goalStates", m.roleHelper.toUzun(m.query));
String template = ConvertTo.readFile(this.getClass().getResource("uzunTemplate.st"));
ArrayList<TRole_Rule> newRules = new ArrayList<TRole_Rule>();
ArrayList<Rule> workableRules = new ArrayList<Rule>();
for (Rule r : m.canAssign.getRules()) {
st.add("rules", new TRedRule_Rule(r, m.roleHelper, m.timeIntervalHelper));
}
workableRules = m.roleHelper.removeEnableDisableRules(m.getAllRules());
for (Rule r : m.canRevoke.getRules()) {
st.add("rules", new TRedRule_Rule(r, m.roleHelper, m.timeIntervalHelper));
}
// Reduce Roles to Integers
m.roleHelper.allowZeroRole = false; // roles start from 1 NOT 0!
m.roleHelper.setupSortedRoles();
// Reduce TimeIntervals to Timeslots
m.timeIntervalHelper.allowZeroTimeslot = false; // time-slots start from t1 NOT t0!
m.timeIntervalHelper.reduceToTimeslots();
for (Rule r : m.canEnable.getRules()) {
st.add("rules", new TRedRule_Rule(r, m.roleHelper, m.timeIntervalHelper));
}
// Convert Query to Reduced ASAPTime SA Query and add any extra rules as needed
TRole_Query query = toTRole_Query(m.query, workableRules, m.roleHelper, m.timeIntervalHelper);
for (Rule r : m.canDisable.getRules()) {
st.add("rules", new TRedRule_Rule(r, m.roleHelper, m.timeIntervalHelper));
// Convert Rules into Reduced ASAPTime NSA Rules
for (Rule r : workableRules) {
newRules.addAll(toTRole_Rules(r, m.roleHelper, m.timeIntervalHelper));
}
logger.fine("Rules: " + m.getAllRules());
logger.fine("Reduced Rules: " + newRules);
// Finalize the Query
query.finalize(m.roleHelper);
ST st = new ST(template);
st.add("numRoles", m.roleHelper.size());
st.add("numTimeSlots", m.timeIntervalHelper.sizeReduced());
st.add("goalStates", query.goalRoles);
st.add("uzunRules", newRules);
convertedStr = st.render();
if (writeToFile) {
File convertedFile = new File(f.getAbsolutePath() + getFileExtenstion());
logger.info("[SAVE OUT]Saving converted format to file: " + convertedFile.getAbsolutePath());
File convertedFile = new File(file.getAbsolutePath() + getFileExtenstion());
if (!convertedFile.exists()) {
convertedFile.createNewFile();
}
Files.write(convertedFile.toPath(), convertedStr.getBytes());
} else {
logger.info("[SAVE OUT] Skipping saving this to file");
}
lastError = null;
} catch (IOException e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.fine(errors.toString());
logger.warning("[ERROR] Unable to save output to file destination!\n" + convertedStr);
lastError = "Error ConvertToRanise.convert.IOException Unable to save converted string to file";
} catch (Exception e) {
StringWriter errors = new StringWriter();
e.printStackTrace(new PrintWriter(errors));
logger.fine(errors.toString());