-
Notifications
You must be signed in to change notification settings - Fork 3
Expand file tree
/
Copy pathexample-input-nuxmv-reals.txt
More file actions
65 lines (60 loc) · 2.15 KB
/
Copy pathexample-input-nuxmv-reals.txt
File metadata and controls
65 lines (60 loc) · 2.15 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
*** This is nuXmv 2.0.0 (compiled on Mon Oct 14 17:48:12 2019)
*** Copyright (c) 2014-2019, Fondazione Bruno Kessler
*** For more information on nuXmv see https://nuxmv.fbk.eu
*** or email to <nuxmv@list.fbk.eu>.
*** Please report bugs at https://nuxmv.fbk.eu/bugs
*** (click on "Login Anonymously" to access)
*** Alternatively write to <nuxmv@list.fbk.eu>.
*** This version of nuXmv is linked to NuSMV 2.6.0.
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Copyright (C) 2010-2019, Fondazione Bruno Kessler
*** This version of nuXmv is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of nuXmv 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
*** This version of nuXmv is linked to MathSAT
*** Copyright (C) 2009-2019 by Fondazione Bruno Kessler
*** Copyright (C) 2009-2019 by University of Trento and others
*** See http://mathsat.fbk.eu
-- no counterexample found with bound 0
-- specification ( G x > 0 | (i > 0 xnor j < 0)) is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample
Trace Type: Counterexample
-> State: 1.1 <-
i = 9
j = 0
x = 1.0
y = 0.0
-> State: 1.2 <-
i = 5
j = 2
x = 0.0
-- no counterexample found with bound 0
-- specification G ((((((-f'1/2 + x) + 1.3e-2) + 0.1E+2) - f'1/3) + f'0/9) + 1) + 2e0 != 0 is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample
Trace Type: Counterexample
-> State: 2.1 <-
i = 9
j = 0
x = 1.0
y = 0.0
-> State: 2.2 <-
i = 5
x = -f'36539/3000
-- no counterexample found with bound 0
-- specification (( F y = (f'1/3 * -f'5/7) / f'11/13 & 0.12 = f'6/50) | 0.12 = -f'12/100) is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample
Trace Type: Counterexample
-- Loop starts here
-> State: 3.1 <-
i = 5
j = 2
x = 1.0
y = 0.0
-> State: 3.2 <-