Commit 465f2381 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

fixed hanging instance after program has finished running

parent c663375a
header {
package mohawk;
import java.util.Vector;
import java.util.Stack;
import java.util.HashMap;
import java.util.Map;
import mohawk.collections.PreCondProcessorInt;
}
class RBACParser extends Parser;
options { k=3; }
{
Vector<String> vRoles;
Vector<String> vUsers;
Vector<String> vAdmin;
Map<Integer, String> mRoleIndex;
Map<String, Integer> mRole2Index;
Map<Integer, String> mUserIndex;
Map<String,Vector<Integer>> mUA;
Map<String,Vector<CREntry>> mCR;
Map<String,Vector<CAEntry>> mCA;
PreCondProcessorInt preCndP;
Stack<Integer> stackOperators;
Vector<String> vSpec; // This vector holds two strings - user and role that will be used in the LTL formulae
// Indices for user and roles while parsing
// Each user has an index corresponding to the order in which the name appears in the list.
int iRoleIndex;
int iUserIndex;
public void initRbac() {
vRoles = new Vector<String>();
vUsers = new Vector<String>();
vAdmin = new Vector<String>();
mRoleIndex = new HashMap<Integer, String>();
mRole2Index = new HashMap<String,Integer>();
mUserIndex = new HashMap<Integer, String>();
mUA = new HashMap<String,Vector<Integer>>();
mCR = new HashMap<String,Vector<CREntry>>();
mCA = new HashMap<String,Vector<CAEntry>>();
vSpec = new Vector<String>();
}
public RBACInstance getRBAC() {
return new RBACInstance(vRoles, vUsers, vAdmin, mUA, mCR, mCA,vSpec);
}
public void setUA(String strUser, String strRole) {
Vector<Integer> vUserUA = mUA.get(strUser);
if(vUserUA == null)
{
vUserUA = new Vector<Integer>();
mUA.put(strUser,vUserUA);
}
int iRoleIndex = mRole2Index.get(strRole); //getMapKey(mRoleIndex, strRole);
vUserUA.add(iRoleIndex);
}
public void addCREntry(String inStrPreCond, String inStrRole) {
CREntry crEntry = new CREntry(inStrPreCond, inStrRole);
Vector<CREntry> vCR = mCR.get(inStrRole);
if(vCR == null)
vCR = new Vector<CREntry>();
vCR.add(new CREntry(inStrPreCond, inStrRole));
mCR.put(inStrRole,vCR);
}
public void addCAEntry(String inStrAdminRole, PreCondition pcPreCond, String inStrRole) {
CAEntry caEntry = new CAEntry(inStrAdminRole, pcPreCond, inStrRole);
Vector<CAEntry> vCA = mCA.get(inStrRole);
if(vCA == null)
vCA = new Vector<CAEntry>();
vCA.add(caEntry);
mCA.put(inStrRole,vCA);
}
/*
private int getMapKey(Map<Integer,String> inMap, String inString) {
for(int i=0; i<inMap.size(); i++) {
if(inMap.get(i).equals(inString)) {
return i;
}
}
System.out.println("Error - BTree::getMapIndex - Value not found in map");
return 0;
}
*/
public void addSpec(String inStrUser, String inStrRole) {
vSpec.add(inStrUser);
vSpec.add(inStrRole);
}
}
roles : ("Roles" {iRoleIndex=0;} ) (n:ID {vRoles.add(n.getText());
mRoleIndex.put(iRoleIndex,n.getText());
mRole2Index.put(n.getText(),iRoleIndex);
iRoleIndex++; })+ SEMI;
users : ("Users" {iUserIndex=0;} ) (u:ID {vUsers.add(u.getText());
mUserIndex.put(iUserIndex,u.getText());
iUserIndex++; })+ SEMI;
ua : "UA" (LANGLE x:ID COMMA y:ID RANGLE { setUA(x.getText(),y.getText()); })+ SEMI;
ca : "CA" (caentry)* SEMI;
caentry : (LANGLE {preCndP = new PreCondProcessorInt(mRole2Index);}) d:ID COMMA e:precondition COMMA f:ID (RANGLE
{
try {
PreCondition pcPreCond = preCndP.result();
addCAEntry(d.getText(), pcPreCond, f.getText());
}catch(Exception e) {
e.printStackTrace();
}
}
);
precondition : atom (COND atom)* | "TRUE";
atom : {int iNeg=0; } (n:NOT { iNeg=1; } )? (a:ID
{
try {
if(iNeg == 0)
preCndP.add(a.getText());
else
preCndP.addNeg(a.getText());
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
);
cr : "CR" (LANGLE mm:ID COMMA nn:ID RANGLE { addCREntry(mm.getText(),nn.getText()); })* SEMI;
admin : "ADMIN" (u:ID { vAdmin.add(u.getText()); })+ SEMI;
spec : "SPEC" (su:ID sr:ID { addSpec(su.getText(),sr.getText()); }) SEMI;
class RBACLexer extends Lexer;
options { k=2;}
ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')*
;
LANGLE : '<'
;
RANGLE : '>'
;
COMMA : ','
;
COND : '&';
NOT : '-';
SEMI : ';';
WS : (' ' | '\t' | '\r' { newline();} | "\r\n" { newline();} | '\n' { newline(); } ) {$setType(Token.SKIP);};
COMMENT : "//" (~( '\n' | '\r' ))* ('\r')? '\n' {$setType(Token.SKIP);} ;
Roles $roles; separator=" "$;
Users $users; separator=" "$;
UA $ua; separator=" "$;
CR $cr; separator=" "$;
CA $ca; separator=" "$;
ADMIN $adminusers; separator=" "$;
SPEC $spec; separator=" "$;
-- This NuSMV specification was automatically generated by the
-- RBAC2SMV tool.
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-- Another user \n" $
-- LTLSPEC
LTLSPEC G ($user$[$roleindex$]=0)
\ No newline at end of file
next($roleindex1$) :=
case
$transition; separator=";\n" $
1 : $roleindex2$;
esac;
\ No newline at end of file
......@@ -94,6 +94,8 @@ public class MohawkMain {
tests.done();
logger.info("[TIMING] " + tests.timing);
results.done();
}
} catch (ParseException e) {
if (logger.getLevel() == Level.FINEST) {
......
......@@ -31,6 +31,17 @@ public class TestingResults {
}
}
public void done() {
try {
if (writer != null) {
writer.close();
}
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
public void addTestResult(TestResults result) {
this.addTestResults(result, true, true);
}
......
......@@ -95,11 +95,14 @@ public class TestingSuite {
absrefine));
try {
logger.info("[RUNNING] Running Mohawk on a testcase:");
result = future.get(smvHelper.TIMEOUT_SECONDS,
TimeUnit.SECONDS);
logger.info("[COMPLETED] Result: " + result
+ ", for the following spec file (in mode "
+ modes.get(j) + "): " + specFile);
/* TIMING */timing.stopTimer(timerName);
} catch (TimeoutException e) {
logger.warning("[TIMEOUT] Mohawk has timed out for SPEC file: "
......@@ -131,6 +134,7 @@ public class TestingSuite {
}
/* TIMING */timing.stopTimer("runTests.mainLoop (" + i + ")");
}
executor.shutdown();
/* TIMING */timing.stopTimer("runTests.mainLoop");
logger.exiting(getClass().getName(), "runTests()");
......
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