Run NuSMV from Java (Linux and Windows)
Windows or Linux
Use this:
- http://commons.apache.org/proper/commons-lang/javadocs/api-release/org/apache/commons/lang3/SystemUtils.html#IS_OS_WINDOWS
- http://commons.apache.org/proper/commons-lang/javadocs/api-release/org/apache/commons/lang3/SystemUtils.html#IS_OS_LINUX
Parse NuSMV Output
- Ignore lines starting with
*** - Ignore empty lines
- A new query starts with
-- specification
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:37:51 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
*** Copyright (c) 2010-2014, Fondazione Bruno Kessler
*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson
-- specification AG !(state = LoopState & c = 13) IN contract1 is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
state = start
contract1.query_c1f1_4 = not_reached
contract1.a = 0
contract1.b = 5
contract1.c = 0
-> Input: 1.2 <-
nextFunc = LoopState
-> State: 1.2 <-
state = LoopState
-> Input: 1.3 <-
nextFunc = SimpleFunction1_func1_ln0
-> State: 1.3 <-
state = SimpleFunction1_func1_ln0
-> Input: 1.4 <-
nextFunc = LoopState
-> State: 1.4 <-
state = SimpleFunction1_func1_ln1
-> Input: 1.5 <-
-> State: 1.5 <-
state = SimpleFunction1_func1_ln2
contract1.c = 5
-> Input: 1.6 <-
-> State: 1.6 <-
state = SimpleFunction1_func1_ln3
contract1.b = 4
-> Input: 1.7 <-
-> State: 1.7 <-
state = SimpleFunction1_func1_ln4
contract1.a = 2
-> Input: 1.8 <-
-> State: 1.8 <-
state = SimpleFunction1_func1_ln5
contract1.query_c1f1_4 = condition_reached
-> Input: 1.9 <-
-> State: 1.9 <-
state = LoopState
-> Input: 1.10 <-
nextFunc = SimpleFunction1_func1_ln0
-> State: 1.10 <-
state = SimpleFunction1_func1_ln0
-> Input: 1.11 <-
nextFunc = LoopState
-> State: 1.11 <-
state = SimpleFunction1_func1_ln1
contract1.query_c1f1_4 = not_reached
-> Input: 1.12 <-
-> State: 1.12 <-
state = SimpleFunction1_func1_ln2
contract1.c = 6
-> Input: 1.13 <-
-> State: 1.13 <-
state = SimpleFunction1_func1_ln3
contract1.b = 3
-> Input: 1.14 <-
-> State: 1.14 <-
state = SimpleFunction1_func1_ln4
-> Input: 1.15 <-
-> State: 1.15 <-
state = SimpleFunction1_func1_ln5
contract1.query_c1f1_4 = condition_reached
-> Input: 1.16 <-
-> State: 1.16 <-
state = LoopState
-> Input: 1.17 <-
nextFunc = SimpleFunction1_func3_ln0
-> State: 1.17 <-
state = SimpleFunction1_func3_ln0
-> Input: 1.18 <-
nextFunc = LoopState
-> State: 1.18 <-
state = SimpleFunction1_func3_ln1
-> Input: 1.19 <-
-> State: 1.19 <-
state = SimpleFunction1_func3_ln2
contract1.a = 10
-> Input: 1.20 <-
-> State: 1.20 <-
state = LoopState
-> Input: 1.21 <-
nextFunc = SimpleFunction1_func1_ln0
-> State: 1.21 <-
state = SimpleFunction1_func1_ln0
-> Input: 1.22 <-
nextFunc = LoopState
-> State: 1.22 <-
state = SimpleFunction1_func1_ln1
contract1.query_c1f1_4 = not_reached
-> Input: 1.23 <-
-> State: 1.23 <-
state = SimpleFunction1_func1_ln2
contract1.c = 13
-> Input: 1.24 <-
-> State: 1.24 <-
state = SimpleFunction1_func1_ln3
contract1.b = 2
-> Input: 1.25 <-
-> State: 1.25 <-
state = SimpleFunction1_func1_ln4
contract1.a = 2
-> Input: 1.26 <-
-> State: 1.26 <-
state = SimpleFunction1_func1_ln5
contract1.query_c1f1_4 = condition_reached
-> Input: 1.27 <-
-> State: 1.27 <-
state = LoopState
-- specification AG !(query_c1f1_4 = condition_confirmed) IN contract1 is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 2.1 <-
state = start
contract1.query_c1f1_4 = not_reached
contract1.a = 0
contract1.b = 5
contract1.c = 0
-> Input: 2.2 <-
nextFunc = LoopState
-> State: 2.2 <-
state = LoopState
-> Input: 2.3 <-
nextFunc = SimpleFunction1_func3_ln0
-> State: 2.3 <-
state = SimpleFunction1_func3_ln0
-> Input: 2.4 <-
nextFunc = LoopState
-> State: 2.4 <-
state = SimpleFunction1_func3_ln1
-> Input: 2.5 <-
-> State: 2.5 <-
state = SimpleFunction1_func3_ln2
contract1.a = 10
-> Input: 2.6 <-
-> State: 2.6 <-
state = LoopState
-> Input: 2.7 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.7 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.8 <-
nextFunc = LoopState
-> State: 2.8 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.9 <-
-> State: 2.9 <-
state = SimpleFunction1_func2_ln2
contract1.b = 15
-> Input: 2.10 <-
-> State: 2.10 <-
state = LoopState
-> Input: 2.11 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.11 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.12 <-
nextFunc = LoopState
-> State: 2.12 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.13 <-
-> State: 2.13 <-
state = SimpleFunction1_func2_ln2
contract1.b = 25
-> Input: 2.14 <-
-> State: 2.14 <-
state = LoopState
-> Input: 2.15 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.15 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.16 <-
nextFunc = LoopState
-> State: 2.16 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.17 <-
-> State: 2.17 <-
state = SimpleFunction1_func2_ln2
contract1.b = 35
-> Input: 2.18 <-
-> State: 2.18 <-
state = LoopState
-> Input: 2.19 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.19 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.20 <-
nextFunc = LoopState
-> State: 2.20 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.21 <-
-> State: 2.21 <-
state = SimpleFunction1_func2_ln2
contract1.b = 45
-> Input: 2.22 <-
-> State: 2.22 <-
state = LoopState
-> Input: 2.23 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.23 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.24 <-
nextFunc = LoopState
-> State: 2.24 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.25 <-
-> State: 2.25 <-
state = SimpleFunction1_func2_ln2
contract1.b = 55
-> Input: 2.26 <-
-> State: 2.26 <-
state = LoopState
-> Input: 2.27 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.27 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.28 <-
nextFunc = LoopState
-> State: 2.28 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.29 <-
-> State: 2.29 <-
state = SimpleFunction1_func2_ln2
contract1.b = 65
-> Input: 2.30 <-
-> State: 2.30 <-
state = LoopState
-> Input: 2.31 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.31 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.32 <-
nextFunc = LoopState
-> State: 2.32 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.33 <-
-> State: 2.33 <-
state = SimpleFunction1_func2_ln2
contract1.b = 75
-> Input: 2.34 <-
-> State: 2.34 <-
state = LoopState
-> Input: 2.35 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.35 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.36 <-
nextFunc = LoopState
-> State: 2.36 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.37 <-
-> State: 2.37 <-
state = SimpleFunction1_func2_ln2
contract1.b = 85
-> Input: 2.38 <-
-> State: 2.38 <-
state = LoopState
-> Input: 2.39 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.39 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.40 <-
nextFunc = LoopState
-> State: 2.40 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.41 <-
-> State: 2.41 <-
state = SimpleFunction1_func2_ln2
contract1.b = 95
-> Input: 2.42 <-
-> State: 2.42 <-
state = LoopState
-> Input: 2.43 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.43 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.44 <-
nextFunc = LoopState
-> State: 2.44 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.45 <-
-> State: 2.45 <-
state = SimpleFunction1_func2_ln2
contract1.b = 105
-> Input: 2.46 <-
-> State: 2.46 <-
state = LoopState
-> Input: 2.47 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.47 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.48 <-
nextFunc = LoopState
-> State: 2.48 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.49 <-
-> State: 2.49 <-
state = SimpleFunction1_func2_ln2
contract1.b = 115
-> Input: 2.50 <-
-> State: 2.50 <-
state = LoopState
-> Input: 2.51 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.51 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.52 <-
nextFunc = LoopState
-> State: 2.52 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.53 <-
-> State: 2.53 <-
state = SimpleFunction1_func2_ln2
contract1.b = 125
-> Input: 2.54 <-
-> State: 2.54 <-
state = LoopState
-> Input: 2.55 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.55 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.56 <-
nextFunc = LoopState
-> State: 2.56 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.57 <-
-> State: 2.57 <-
state = SimpleFunction1_func2_ln2
contract1.b = 135
-> Input: 2.58 <-
-> State: 2.58 <-
state = LoopState
-> Input: 2.59 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.59 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.60 <-
nextFunc = LoopState
-> State: 2.60 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.61 <-
-> State: 2.61 <-
state = SimpleFunction1_func2_ln2
contract1.b = 145
-> Input: 2.62 <-
-> State: 2.62 <-
state = LoopState
-> Input: 2.63 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.63 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.64 <-
nextFunc = LoopState
-> State: 2.64 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.65 <-
-> State: 2.65 <-
state = SimpleFunction1_func2_ln2
contract1.b = 155
-> Input: 2.66 <-
-> State: 2.66 <-
state = LoopState
-> Input: 2.67 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.67 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.68 <-
nextFunc = LoopState
-> State: 2.68 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.69 <-
-> State: 2.69 <-
state = SimpleFunction1_func2_ln2
contract1.b = 165
-> Input: 2.70 <-
-> State: 2.70 <-
state = LoopState
-> Input: 2.71 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.71 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.72 <-
nextFunc = LoopState
-> State: 2.72 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.73 <-
-> State: 2.73 <-
state = SimpleFunction1_func2_ln2
contract1.b = 175
-> Input: 2.74 <-
-> State: 2.74 <-
state = LoopState
-> Input: 2.75 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.75 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.76 <-
nextFunc = LoopState
-> State: 2.76 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.77 <-
-> State: 2.77 <-
state = SimpleFunction1_func2_ln2
contract1.b = 185
-> Input: 2.78 <-
-> State: 2.78 <-
state = LoopState
-> Input: 2.79 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.79 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.80 <-
nextFunc = LoopState
-> State: 2.80 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.81 <-
-> State: 2.81 <-
state = SimpleFunction1_func2_ln2
contract1.b = 195
-> Input: 2.82 <-
-> State: 2.82 <-
state = LoopState
-> Input: 2.83 <-
nextFunc = SimpleFunction1_constructor_ln0
-> State: 2.83 <-
state = SimpleFunction1_constructor_ln0
-> Input: 2.84 <-
nextFunc = LoopState
-> State: 2.84 <-
state = SimpleFunction1_constructor_ln1
-> Input: 2.85 <-
-> State: 2.85 <-
state = SimpleFunction1_constructor_ln2
contract1.a = 3
-> Input: 2.86 <-
-> State: 2.86 <-
state = LoopState
-> Input: 2.87 <-
nextFunc = SimpleFunction1_func2_ln0
-> State: 2.87 <-
state = SimpleFunction1_func2_ln0
-> Input: 2.88 <-
nextFunc = LoopState
-> State: 2.88 <-
state = SimpleFunction1_func2_ln1
-> Input: 2.89 <-
-> State: 2.89 <-
state = SimpleFunction1_func2_ln2
contract1.b = 198
-> Input: 2.90 <-
-> State: 2.90 <-
state = LoopState
-> Input: 2.91 <-
nextFunc = SimpleFunction1_func1_ln0
-> State: 2.91 <-
state = SimpleFunction1_func1_ln0
-> Input: 2.92 <-
nextFunc = LoopState
-> State: 2.92 <-
state = SimpleFunction1_func1_ln1
-> Input: 2.93 <-
-> State: 2.93 <-
state = SimpleFunction1_func1_ln2
contract1.c = 1
-> Input: 2.94 <-
-> State: 2.94 <-
state = SimpleFunction1_func1_ln3
contract1.b = 197
-> Input: 2.95 <-
-> State: 2.95 <-
state = SimpleFunction1_func1_ln4
contract1.a = 2
-> Input: 2.96 <-
-> State: 2.96 <-
state = SimpleFunction1_func1_ln5
contract1.query_c1f1_4 = condition_reached
-> Input: 2.97 <-
-> State: 2.97 <-
state = LoopState
contract1.query_c1f1_4 = condition_confirmed