Commit 61cf66f3 authored by Jonathan Shahen's avatar Jonathan Shahen

hotfix to pull in changes from Ubuntu instance

parent de89aff7
The MIT License
Copyright (c) 2010 Karthick Jayaraman
Copyright (c) 2014 Jonathan Shahen
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
......
package mohawk;
import java.io.BufferedReader;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.util.ArrayList;
import java.util.Scanner;
import org.apache.commons.cli.Options;
public class MohawkCUI {
public static String previousCommandFilename = "MohawkCUIPreviousCommand.txt";
public static void main(String[] args) {
MohawkInstance inst = new MohawkInstance();
ArrayList<String> argv = new ArrayList<String>();
......@@ -20,8 +26,10 @@ public class MohawkCUI {
System.out.print("Enter Commandline Argument ('!exit' to run): ");
String quotedStr = "";
StringBuilder fullCommand = new StringBuilder();
while (true) {
cmd = user_input.next();
fullCommand.append(cmd + " ");
if (quotedStr.isEmpty() && cmd.startsWith("\"")) {
System.out.println("Starting: " + cmd);
......@@ -49,6 +57,15 @@ public class MohawkCUI {
System.out.println("Commands: " + argv);
FileWriter fw;
try {
fw = new FileWriter(previousCommandFilename, false);
fw.write(fullCommand.toString());
fw.close();
} catch (IOException e) {
System.out.println("[ERROR] Unable to write out previous command to: " + previousCommandFilename);
}
inst.run(argv.toArray(new String[1]));
}
......@@ -67,5 +84,14 @@ public class MohawkCUI {
System.out.println("");
System.out.println("-mode bmc -run all -bulk -input data/tests !exit");
System.out.println("-mode bmc -run smv -bulk -input data/tests !exit");
System.out.println("");
try {
BufferedReader bfr = new BufferedReader(new FileReader(previousCommandFilename));
String previousCmd = bfr.readLine();
bfr.close();
System.out.println("Previous Command: " + previousCmd);
} catch (IOException e) {
System.out.println("[ERROR] Unable to load previous command!");
}
}
}
......@@ -101,6 +101,10 @@ public class MohawkInstance {
logger.info("[ACTION] Will only convert the testcase provided");
tests.onlyConvertSpecToSmvFormat();
break;
case "dia":
logger.info("[ACTION] Will only calculate the estimated diameter of the testcase provided");
tests.calculateDiameter();
break;
default:
logger.severe("The Run Option '" + runVal + "' has not been implemented. "
+ "Please see use 'mohawk -help' to see which Run Options have been implemented");
......@@ -234,9 +238,9 @@ public class MohawkInstance {
// Add Actionable Options
options.addOption(OptionBuilder
.withArgName("all|smv")
.withArgName("all|smv|dia")
.withDescription(
"Runs the whole model checker when equal to 'all'; Runs only the SMV conversion when equal to 'smv'")
"Runs the whole model checker when equal to 'all'; Runs only the SMV conversion when equal to 'smv'; Calculates the diameter when equal to 'dia'")
.hasArg().create(OptionString.RUN.toString()));
}
......
......@@ -4,8 +4,11 @@
package mohawk.math;
import java.io.File;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import java.util.logging.Logger;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
......@@ -15,6 +18,7 @@ import mohawk.rbac.RBACSpecReader;
*
*/
public class CalculateDiameter {
public final static Logger logger = Logger.getLogger("mohawk");
// public CalculateDiameter() {}
......@@ -44,7 +48,7 @@ public class CalculateDiameter {
CalculateRplus crplus = new CalculateRplus(rbac);
CalculateRplusOnly crplusonly = new CalculateRplusOnly(rbac);
CalculateRMax rmax = new CalculateRMax(rbac);
//CalculateRMax rmax = new CalculateRMax(rbac);
Set<String> R_plus = crplus.getRPlus();
Set<String> R_minus = crplus.getRMinus();
Set<String> RevRoles = crplus.CalIrrevocableRoles();
......@@ -64,13 +68,12 @@ public class CalculateDiameter {
System.out.println("Union of Tightenings : " + RUnionRoles.size());
}
public int GetDiameter(RBACInstance rbacinstance) {
public static int GetDiameter(RBACInstance rbacinstance) {
RBACInstance rbac = rbacinstance;
int no_roles = rbac.getNumRoles();
CalculateRplus crplus = new CalculateRplus(rbac);
CalculateRplusOnly crplusonly = new CalculateRplusOnly(rbac);
CalculateRMax rmax = new CalculateRMax(rbac);
//CalculateRMax rmax = new CalculateRMax(rbac);
Set<String> R_plus = crplus.getRPlus();
Set<String> R_minus = crplus.getRMinus();
Set<String> RevRoles = crplus.CalIrrevocableRoles();
......@@ -92,13 +95,16 @@ public class CalculateDiameter {
return ((int) Math.pow(2, (no_roles - tightenings)) - 1 + tightenings);
}
public void CalDiameterFile(String filename) {
public static Map<String, Integer> CalDiameterFile(String filename) {
File rbacfile = new File(filename);
return CalDiameterFile(rbacfile);
}
public static Map<String, Integer> CalDiameterFile(File rbacfile) {
if (!rbacfile.exists()) {
System.out.println("The RBAC specification file " + rbacfile + " does not exists.");
return;
return null;
}
/*
......@@ -109,17 +115,18 @@ public class CalculateDiameter {
// RBACParser parser = new RBACParser(lexer);
RBACInstance rbac = null;
RBACSpecReader rbacreader = new RBACSpecReader(filename);
RBACSpecReader rbacreader = new RBACSpecReader(rbacfile.getAbsolutePath());
rbac = rbacreader.getRBAC();
int no_roles = rbac.getNumRoles();
CalculateRplus crplus = new CalculateRplus(rbac);
CalculateRplusOnly crplusonly = new CalculateRplusOnly(rbac);
CalculateRMax rmax = new CalculateRMax(rbac);
//CalculateRMax rmax = new CalculateRMax(rbac);
Set<String> R_plus = crplus.getRPlus();
Set<String> R_minus = crplus.getRMinus();
Set<String> RevRoles = crplus.CalIrrevocableRoles();
Set<String> R_plusonly = crplusonly.getRplusOnly();
Set<String> RMaxRoles = rmax.CalRMax();
//Set<String> RMaxRoles = rmax.CalRMax();
Set<String> RUnionRoles = new HashSet<String>();
RUnionRoles.addAll(R_plus);
RUnionRoles.addAll(R_minus);
......@@ -130,7 +137,16 @@ public class CalculateDiameter {
System.out.println("Tightening 2 - R+ : " + R_plus.size());
System.out.println("Tightening 3 - R_p : " + R_plusonly.size());
System.out.println("Tightening 4 - R_irrev : " + RevRoles.size());
System.out.println("Tightening 5 - R_max : " + RMaxRoles.size());
//System.out.println("Tightening 5 - R_max : " + RMaxRoles.size());
System.out.println("Union of Tightenings : " + RUnionRoles.size());
int tightenings = RUnionRoles.size();
int diameter = ((int) Math.pow(2, (no_roles - tightenings)) - 1 + tightenings);
Map<String, Integer> ret = new HashMap<String, Integer>();
ret.put("Diameter", diameter);
ret.put("NumRoles", no_roles);
ret.put("NumTightenings", RUnionRoles.size());
return ret;
}
}
......@@ -6,6 +6,7 @@ package mohawk.math;
import java.util.HashSet;
import java.util.Set;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.rbac.RBACInstance;
......@@ -15,6 +16,7 @@ import mohawk.rbac.RBACInstance;
*
*/
public class CalculateRMax {
public final static Logger logger = Logger.getLogger("mohawk");
RBACInstance rbac_instance;
......
......@@ -8,6 +8,7 @@ import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
......@@ -19,6 +20,7 @@ import mohawk.rbac.RBACInstance;
*
*/
public class CalculateRplus {
public final static Logger logger = Logger.getLogger("mohawk");
RBACInstance rbac_instance;
Set<String> R_plus;
......
......@@ -8,6 +8,7 @@ import java.util.Iterator;
import java.util.LinkedList;
import java.util.Set;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.pieces.PreCondition;
......@@ -18,6 +19,7 @@ import mohawk.rbac.RBACInstance;
*
*/
public class CalculateRplusOnly {
public final static Logger logger = Logger.getLogger("mohawk");
RBACInstance rbac_instance;
Set<String> R_pos;
......
......@@ -28,6 +28,7 @@ import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.collections.RoleDepTree;
import mohawk.pieces.CAEntry;
......@@ -39,6 +40,7 @@ import mohawk.rbac.RBACInstance;
*
*/
public class EstimateDia {
public final static Logger logger = Logger.getLogger("mohawk");
RBACInstance rbac_instance;
RoleDepTree rdeptree;
......
......@@ -29,6 +29,7 @@ import java.io.IOException;
import java.io.InputStreamReader;
import java.util.Arrays;
import java.util.List;
import java.util.logging.Logger;
/**
* @author kjayaram
......@@ -39,11 +40,13 @@ import java.util.List;
*
*/
public class NuSMV {
public final static Logger logger = Logger.getLogger("mohawk");
public static Process execProcess = null;
/**
*
*/
*
*/
public NuSMV() {
}
......
......@@ -36,6 +36,8 @@ import mohawk.rbac.RBACPAT;
/**
* @author Karthick Jayaraman
*
* STAND ALONE
*
*/
public class CnvRBACPAT {
......
......@@ -9,7 +9,6 @@ import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.Map;
import java.util.Random;
import java.util.Vector;
import mohawk.pieces.CAEntry;
......@@ -30,9 +29,6 @@ public class WriteRBACSpec {
// RBAC instance to write to file.
private RBACInstance rbacinstance;
// Random Number Generator
private Random rndGen;
public WriteRBACSpec(String filename) {
try {
String strTemplateString = this.getTemplateStr(filename);
......@@ -40,8 +36,6 @@ public class WriteRBACSpec {
} catch (IOException e) {
e.printStackTrace();
}
// Initialize Random number generator
rndGen = new Random();
}
private String getTemplateStr(String filename) throws IOException {
......
......@@ -24,6 +24,7 @@
package mohawk.pieces;
/**
* This class represents a CAEntry. Each CAEntry has three parts: - Roles that the administrator should have -
* Preconditions, which are essentially set of roles the user should have Preconditions on roles are specified as a
......@@ -32,7 +33,6 @@ package mohawk.pieces;
* @author Karthick Jayaraman
*/
public class CAEntry {
private String strAdminRole;
private PreCondition pcPreconditions;
private String strRole;
......
......@@ -33,7 +33,6 @@ import java.util.Set;
*
*/
public class PreCondition {
private Map<Integer, Integer> mBitVector;
public PreCondition() {
......
......@@ -48,9 +48,10 @@ import antlr.TokenStreamException;
/**
* @author Karthick Jayaraman This is the main class that will serve as an entry point to the tool.
*
* STAND ALONE
*
*/
public class RBAC2SMV {
/**
* @param args
*
......
......@@ -9,6 +9,7 @@ package mohawk.rbac;
import java.util.HashMap;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
......@@ -19,6 +20,7 @@ import mohawk.pieces.CREntry;
*
*/
public class RBACInstance {
public final static Logger logger = Logger.getLogger("mohawk");
private Vector<String> vRoles;
private Vector<String> vUsers;
......
......@@ -26,6 +26,7 @@ import antlr.TokenStreamException;
/**
* @author Karthick Jayaraman
*
* PART OF CnvRBACPAT (STANDALONE)
*/
public class RBACPAT {
......
......@@ -8,6 +8,7 @@ import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.Reader;
import java.io.StringReader;
import java.util.logging.Logger;
import mohawk.rbac.generated.RBACLexer;
import mohawk.rbac.generated.RBACParser;
......@@ -19,6 +20,7 @@ import antlr.TokenStreamException;
*
*/
public class RBACSpecReader {
public final static Logger logger = Logger.getLogger("mohawk");
private RBACInstance rbac;
......
......@@ -24,6 +24,7 @@
package mohawk.refine;
import java.io.File;
import java.util.logging.Logger;
import mohawk.collections.NuSMVMode;
import mohawk.rbac.RBACInstance;
......@@ -34,6 +35,7 @@ import mohawk.rbac.RBACSpecReader;
*
*/
public class AbsRefine {
public final static Logger logger = Logger.getLogger("mohawk");
public void refine(String specfile) {
refine(specfile, null);
......
......@@ -30,6 +30,7 @@ import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
......@@ -39,8 +40,10 @@ import mohawk.rbac.RBACInstance;
/**
* @author Karthick Jayaraman
*
* NOT USED
*/
public class FwdPruning {
public final static Logger logger = Logger.getLogger("mohawk");
RBACInstance unsliced;
RBACInstance sliced;
......
......@@ -11,6 +11,7 @@ import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.collections.NuSMVMode;
import mohawk.collections.RoleDepTree;
......@@ -29,6 +30,7 @@ import mohawk.rbac.RBACInstance;
*
*/
public class RolesAbsRefine {
public final static Logger logger = Logger.getLogger("mohawk");
public RolesAbsRefine(RBACInstance inRbac) {
......@@ -316,17 +318,17 @@ public class RolesAbsRefine {
}
// NuSMV bmc mode
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(nextinstance);
int bound = CalculateDiameter.GetDiameter(nextinstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
nextinstance.getNumRoles(), bound));
// NuSMV bmc
Boolean result;
if (mode == NuSMVMode.BMC)
if (mode == NuSMVMode.BMC) {
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
else
} else {
result = NuSMV.SMC(nusmv.getNuSMVCode());
}
if (result) {
System.out.println("Found counter example in step " + (fileno));
......
......@@ -11,6 +11,7 @@ import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
......@@ -22,6 +23,7 @@ import mohawk.rbac.RBACInstance;
*
*/
public class RoleSlicer {
public final static Logger logger = Logger.getLogger("mohawk");
private RBACInstance unsliced;
private RBACInstance sliced;
......
......@@ -7,6 +7,7 @@ import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
......@@ -17,6 +18,7 @@ import mohawk.rbac.RBACInstance;
*
*/
public class SliceQueryRole {
public final static Logger logger = Logger.getLogger("mohawk");
private RBACInstance unsliced;
private RBACInstance sliced;
......
......@@ -5,6 +5,7 @@ import java.io.IOException;
import java.io.PrintWriter;
import java.io.StringWriter;
import java.util.ArrayList;
import java.util.Map;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
......@@ -19,6 +20,7 @@ import mohawk.global.results.ExecutionResult;
import mohawk.global.results.MohawkResults;
import mohawk.global.timing.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.math.CalculateDiameter;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
import mohawk.refine.RolesAbsRefine;
......@@ -233,4 +235,31 @@ public class TestingSuite {
logger.exiting(getClass().getName(), "onlyConvertSpecToSmvFormat()");
}
/**
* Displays the calculated Diameter of input RBAC Spec Files
*
* @throws IOException
*/
public void calculateDiameter() throws IOException {
logger.entering(getClass().getName(), "calculateDiameter()");
smvHelper.loadSpecFiles();
Map<String, Integer> diameter;
for (int i = 0; i < smvHelper.specFiles.size(); i++) {
File specFile = smvHelper.specFiles.get(i);
diameter = CalculateDiameter.CalDiameterFile(specFile);
if (diameter == null) {
logger.log(Level.SEVERE, "[DIAMETER] Error calculating diameter for {1}", specFile.getAbsolutePath());
} else {
logger.log(
Level.INFO,
"[DIAMETER] Diameter: {0}, Roles: {1}, Tightenings: {2}, File: {3}",
new Object[] { diameter.get("Diameter"), diameter.get("NumRoles"),
diameter.get("NumTightenings"), specFile.getAbsolutePath() });
}
}
logger.exiting(getClass().getName(), "calculateDiameter()");
}
}
......@@ -7,6 +7,7 @@ import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.Reader;
import java.util.logging.Logger;
import mohawk.output.WriteRBACSpec;
import mohawk.rbac.RBACInstance;
......@@ -17,8 +18,11 @@ import antlr.RecognitionException;
/**
* @author Karthick Jayaraman
*
* STAND ALONE
*
*/
public class RemoveCR {
public final static Logger logger = Logger.getLogger("mohawk");
/**
* @param args
......
......@@ -5,6 +5,7 @@ import java.io.IOException;
import java.util.HashMap;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.output.WriteRBACSpec;
import mohawk.pieces.CAEntry;
......@@ -13,7 +14,15 @@ import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
/**
*
* @author Karthick Jayaraman
*
* STAND ALONE
*/
public class Replicate {
public final static Logger logger = Logger.getLogger("mohawk");
/**
* @param args
......
......@@ -18,6 +18,8 @@ import mohawk.slicer.RoleSlicer;
/**
* @author kjayaram
*
* STAND ALONE
*
*/
public class RoleAnalysis {
......
......@@ -11,6 +11,7 @@ import java.util.Collection;
import java.util.Iterator;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
......@@ -24,6 +25,7 @@ import antlr.RecognitionException;
*
*/
public class SizeOfRBAC {
public final static Logger logger = Logger.getLogger("mohawk");
/**
* @param args
......
......@@ -9,6 +9,7 @@ import java.util.Collection;
import java.util.Iterator;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Logger;
import mohawk.output.WriteRBACSpec;
import mohawk.pieces.CAEntry;
......@@ -23,6 +24,7 @@ import mohawk.slicer.SliceQueryRole;
*
*/
public class Slicer {
public final static Logger logger = Logger.getLogger("mohawk");
/**
* @param args
......
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