- Dec 26, 2016
-
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
- Nov 21, 2016
-
-
Jonathan Shahen authored
-
- Nov 14, 2016
-
-
Jonathan Shahen authored
-
- May 31, 2016
-
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
- May 05, 2016
-
-
Jonathan Shahen authored
-
- Jan 17, 2016
-
-
Jonathan Shahen authored
-
Jonathan Shahen authored
Comments; hiding debugging messages in IF statements; adding more logging levels; Outputting the TIMEOUT each time (I think this isn't working)
-
Jonathan Shahen authored
-
- Jan 16, 2016
-
-
Jonathan Shahen authored
Adding 3 Heuristics and 1 new optimization to Mohawk 2.0 (regression tests pass, still need to test ASASPTIME tests)
-
Jonathan Shahen authored
Moving function convertSpecToSMVFormat() out of SMVSpecHelper and into the TestingSuite and adding better error warning into CalculateDiameter
-
Jonathan Shahen authored
-
- Jan 15, 2016
-
-
Jonathan Shahen authored
Setting up Heuristics to make quicker decisions without having to convert to NuSMv and without having to run it through the NuSMv SAT solver Heuristic #1: returns GOAL_UNREACHABLE if the SPC role cannot be found in the target role of any CA rule (see heuristic1.spec for an example) Heuristic #2: return GOAL_REACHABLE if there is a CA rule that has the target role equal to the SPEC role and that rule is 'startable' (ONLY negative preconditions or TRUE)
-
Jonathan Shahen authored
Allowing for a choice between version for outputting the NuSMV format; WARNING: version 2 is not complete and should not be used until it is finished and tested
-
Jonathan Shahen authored
Forgot to add this last time; separated out the different version of SMV templates; required for the build script to work
-
Jonathan Shahen authored
-
- Jan 08, 2016
-
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
- Dec 21, 2015
-
-
Jonathan Shahen authored
-
Jonathan Shahen authored
Adds stats to the SMV files, useful to know how many roles have no transitions besides staying at FALSE; This will be used to show the possibilities of a future optimization
-
- Dec 20, 2015
-
-
Jonathan Shahen authored
Lots of iterative work to find the bug....currently it looks like it is the NuSMV version 2.5.4 that is buggy, but these bug hunt changes do provide much needed cleanup to the code (see the singleton MohawkSettings)
-
Jonathan Shahen authored
-
Jonathan Shahen authored
HOTFIX: error occurred when slicing that would reorder the roles and there was an assumption that the last role is the admin role, so it incorrectly added an extra role to the sliced roles list instead of the admin role. This is fixed by iterating through the CA rules and adding a set of admin roles to the sliced RBAC instance. NOTE: the old code assumed that there could be only 1 admin role, this code allows for multiple admin roles (this might not be needed and if it isn't then the code can be optimized to search for the first CA with a Admin Role and then stop searching and adding every role to a set)
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
- Dec 15, 2015
-
-
Jonathan Shahen authored
Bug data added; this is required to show the bug that occurs when SkipRefine is turned ON; remove from repo after bug is fixed!
-
- Dec 14, 2015
-
-
Jonathan Shahen authored
Moving the regression test to mohawk.test; formatting the regression tests; changed positive3 to Ahn's test and positive4 to one of the converted files from NSA
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
- Dec 09, 2015
-
-
Jonathan Shahen authored
Writes out the SMV file always and now can call NuSMV with the file's name instead writing the file contents in a pipe
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
- Dec 08, 2015
-
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
Jonathan Shahen authored
-
- Nov 13, 2015
-
-
Jonathan Shahen authored
-
Jonathan Shahen authored
Ability to write out each SMV file, currently deactivated (must manually change this - only do this if you want to manually run NuSMV), also now writes out (can disable) the rule that created each NuSMV NEXT case
-
Jonathan Shahen authored
-
Jonathan Shahen authored
Better Error Control (remember that logger.severe does not cut the program there, it will continue running so throw a new error after reporting it)
-