Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Open sidebar
Jon Shahen
mohawk-2.0
Commits
9a19cfe3
Commit
9a19cfe3
authored
Oct 15, 2014
by
Jonathan Shahen
Browse files
MOHAWK-1 #time 2h
MOHAWK-1 #done
parent
200a124a
Pipeline
#7931
skipped
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
82 additions
and
25 deletions
+82
-25
mohawk.log
mohawk.log
+4
-0
src/mohawk/AbsRefine.java
src/mohawk/AbsRefine.java
+3
-1
src/mohawk/BoundedModelChecking.java
src/mohawk/BoundedModelChecking.java
+3
-4
src/mohawk/MohawkMain.java
src/mohawk/MohawkMain.java
+72
-20
No files found.
mohawk.log
0 → 100644
View file @
9a19cfe3
<?xml version="1.0" encoding="windows-1252" standalone="no"?>
<!DOCTYPE log SYSTEM "logger.dtd">
<log>
</log>
src/mohawk/AbsRefine.java
View file @
9a19cfe3
...
...
@@ -50,8 +50,10 @@ public class AbsRefine {
RBACInstance
rbac
=
reader
.
getRBAC
();
RolesAbsRefine
absrefine
=
new
RolesAbsRefine
(
rbac
);
if
(
mode
!
=
null
)
if
(
mode
=
=
null
)
absrefine
.
setMode
(
NuSMVMode
.
SMC
);
// Set the SMC mode
else
absrefine
.
setMode
(
mode
);
absrefine
.
absrefineloop
();
}
}
src/mohawk/BoundedModelChecking.java
View file @
9a19cfe3
...
...
@@ -34,8 +34,7 @@ import java.io.IOException;
import
java.io.InputStreamReader
;
/**
* @author Karthick Jayaraman This class is responsible for runnning NuSMV in
* the BMC mode.
* @author Karthick Jayaraman
*/
public
class
BoundedModelChecking
{
...
...
@@ -66,8 +65,8 @@ public class BoundedModelChecking {
execProcess
.
getOutputStream
().
flush
();
execProcess
.
getOutputStream
().
close
();
bufread
=
new
BufferedReader
(
new
InputStreamReader
(
execProcess
.
getInputStream
()));
bufread
=
new
BufferedReader
(
new
InputStreamReader
(
execProcess
.
getInputStream
()));
String
strLine
=
null
;
while
((
strLine
=
bufread
.
readLine
())
!=
null
)
{
...
...
src/mohawk/MohawkMain.java
View file @
9a19cfe3
package
mohawk
;
import
java.io.BufferedReader
;
import
java.io.File
;
import
java.io.IOException
;
import
java.io.InputStreamReader
;
import
java.text.SimpleDateFormat
;
import
java.util.logging.ConsoleHandler
;
import
java.util.logging.FileHandler
;
import
java.util.logging.Level
;
import
java.util.logging.Logger
;
import
java.util.logging.SimpleFormatter
;
import
org.apache.commons.cli.BasicParser
;
import
org.apache.commons.cli.CommandLine
;
...
...
@@ -23,11 +27,22 @@ import org.apache.commons.cli.ParseException;
public
class
MohawkMain
{
public
final
static
Logger
logger
=
Logger
.
getLogger
(
"mohawk"
);
public
static
String
NuSMV_filepath
=
"NuSMV"
;
public
static
String
NuSMV_filepath
=
"NuSMV
2
"
;
public
static
SimpleDateFormat
SDF
=
new
SimpleDateFormat
(
"yyyy-MM-dd_HH-mm-ss-SSS"
);
public
static
String
SMV_filepath
=
"latestRBAC2SMV.smv"
;
public
static
String
Logger_filepath
=
"mohawk.log"
;
private
static
ConsoleHandler
handler
=
new
ConsoleHandler
();
private
static
Level
LoggerLevel
;
private
static
FileHandler
fileHandler
;
public
static
Level
getLoggerLevel
()
{
return
LoggerLevel
;
}
public
static
void
setLoggerLevel
(
Level
loggerLevel
)
{
LoggerLevel
=
loggerLevel
;
}
@SuppressWarnings
(
"static-access"
)
public
static
void
main
(
String
[]
args
)
{
...
...
@@ -38,7 +53,7 @@ public class MohawkMain {
options
.
addOption
(
"help"
,
false
,
"print this message"
);
options
.
addOption
(
"version"
,
false
,
"print the version information and exit"
);
options
.
addOption
(
"checknus
v
m"
,
false
,
options
.
addOption
(
"checknusm
v
"
,
false
,
"checks that NuSMV is installed on the system"
);
// Add Logging Level Options
...
...
@@ -86,10 +101,10 @@ public class MohawkMain {
options
.
addOption
(
"smvdelete"
,
false
,
"Delete the SMV file when the operation is complete"
);
options
.
addOption
(
OptionBuilder
.
withArgName
(
"
y/n/b
"
)
.
withArgName
(
"
bmc|smc
"
)
.
withDescription
(
"Uses the Bound Estimation when equal to '
y
'; Uses
NuSMV's default bounds of 10 when equal to 'n'; Runs both tests
when equal to '
b
'"
)
.
hasArg
().
create
(
"
bmc
"
));
"Uses the Bound Estimation
Checker
when equal to '
bmc
'; Uses
Symbolic Model Checking
when equal to '
smc
'"
)
.
hasArg
().
create
(
"
mode
"
));
// Add Actionable Options
options
.
addOption
(
OptionBuilder
...
...
@@ -103,15 +118,19 @@ public class MohawkMain {
CommandLine
cmd
=
parser
.
parse
(
options
,
args
);
// Logging Level
handler
.
setFormatter
(
new
SimpleFormatter
());
if
(
cmd
.
hasOption
(
"quiet"
))
{
l
ogger
.
set
Level
(
Level
.
SEVERE
);
setL
oggerLevel
(
Level
.
SEVERE
);
}
else
if
(
cmd
.
hasOption
(
"debug"
))
{
l
ogger
.
set
Level
(
Level
.
FINEST
);
setL
oggerLevel
(
Level
.
FINEST
);
}
else
if
(
cmd
.
hasOption
(
"verbose"
))
{
l
ogger
.
set
Level
(
Level
.
INFO
);
setL
oggerLevel
(
Level
.
INFO
);
}
else
{
l
ogger
.
set
Level
(
Level
.
WARNING
);
setL
oggerLevel
(
Level
.
WARNING
);
}
logger
.
setLevel
(
LoggerLevel
);
handler
.
setLevel
(
LoggerLevel
);
logger
.
addHandler
(
handler
);
// Custom Configuration
if
(
cmd
.
hasOption
(
"numsmv"
))
{
...
...
@@ -127,10 +146,39 @@ public class MohawkMain {
f
.
printHelp
(
"mohawk"
,
options
,
true
);
return
;
}
else
if
(
cmd
.
hasOption
(
"version"
))
{
System
.
out
.
println
(
"2.0.0"
);
logger
.
info
(
"2.0.0"
);
return
;
}
else
if
(
cmd
.
hasOption
(
"checknusvm"
))
{
}
else
if
(
cmd
.
hasOption
(
"checknusmv"
))
{
logger
.
fine
(
"Checking the NuSMV version number"
);
String
[]
commands
=
{
NuSMV_filepath
,
"-help"
};
ProcessBuilder
pb
=
new
ProcessBuilder
(
commands
);
pb
.
redirectErrorStream
(
true
);
// REQUIRED: NuSVM uses STDERR
try
{
// will throw error if it cannot find NuSMV
Process
proc
=
pb
.
start
();
BufferedReader
br
=
new
BufferedReader
(
new
InputStreamReader
(
proc
.
getInputStream
()));
String
strLine
=
null
;
if
(
br
.
ready
())
{
while
((
strLine
=
br
.
readLine
())
!=
null
)
{
if
(
strLine
.
contains
(
"This is NuSMV"
))
{
logger
.
info
(
strLine
);
break
;
}
}
}
else
{
logger
.
warning
(
"No output was given by NuSMV, "
+
"maybe the commandline arguments have changed "
+
"or the file "
+
NuSMV_filepath
+
" points to the wrong file"
);
}
}
catch
(
IOException
e
)
{
logger
.
severe
(
"No Version of NuSMV was found, "
+
"please check that NuSMV is on the PATH."
);
return
;
}
}
// Set IO Configurations
...
...
@@ -157,18 +205,22 @@ public class MohawkMain {
Logger_filepath
=
logfile
.
getAbsolutePath
();
}
}
// Add
try
{
if
(!
Logger_filepath
.
isEmpty
())
{
logger
.
addHandler
(
new
FileHandler
(
Logger_filepath
));
}
}
catch
(
Exception
e
)
{
logger
.
severe
(
e
.
getMessage
());
return
;
// Add Logger File Handler
if
(!
Logger_filepath
.
isEmpty
())
{
fileHandler
=
new
FileHandler
(
Logger_filepath
);
fileHandler
.
setLevel
(
getLoggerLevel
());
logger
.
addHandler
(
fileHandler
);
}
// Execute the test cases
if
(
cmd
.
hasOption
(
"run"
))
{
logger
.
fine
(
"TODO: Write the 'run' parameter"
);
}
}
catch
(
ParseException
e
)
{
logger
.
severe
(
e
.
getMessage
());
}
catch
(
Exception
e
)
{
logger
.
severe
(
e
.
getMessage
());
return
;
}
}
}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment