Run NuSMV from Java (Linux and Windows) (#19) · Issues · Jon Shahen / Solidity-Safety to Model Checking

Run NuSMV from Java (Linux and Windows)

## Windows or Linux Use this: 1. http://commons.apache.org/proper/commons-lang/javadocs/api-release/org/apache/commons/lang3/SystemUtils.html#IS_OS_WINDOWS 1. 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 ```

issue