c model ISR_TJ
c  /home/toda/src/NuSMV-2.6.0-Linux_untouched/binary/bin/NuSMV -bmc -bmc_length 100 -n 0 /home/toda/2022solver/bin/../tmp/sp001_01.smv > sp001_01.log
c ECC Heuristic Algorithm by Alessio Conte, Roberto Grossi and Andrea Marino. University of Pisa.
c This code is compiled using Java 1.8
c Parsing: 13
c Reading graph from file..
c Removing duplicates.................
c Done.
c Algotithm object created, class=it.unipi.di.clq.eps.lists.EPSc
c Edges: 66
c 0 cliques
c 2 cliques
c 4 cliques
c The solution is correct.
c Cliques: 8
c Sum: 40
c MaxSize: 0
c Time: 12
c Aborted: false
c ML = 12
c SIZE = 13
c Removed 0 cliques to minimalize solution.
c Result saved!
c Clique size distribution: {[2,2][6,6]}
c NODE covering index distribution:{[2,3][3,6][4,4]}
c EDGE covering index distrubution:{[1,44][2,18][3,4]}
c Total edges:66
c Distributions saved!
c *** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015)
c *** Enabled addons are: compass
c *** For more information on NuSMV see <http://nusmv.fbk.eu>
c *** or email to <nusmv-users@list.fbk.eu>.
c *** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
c 
c *** Copyright (c) 2010-2014, Fondazione Bruno Kessler
c 
c *** This version of NuSMV is linked to the CUDD library version 2.4.1
c *** Copyright (c) 1995-2004, Regents of the University of Colorado
c 
c *** This version of NuSMV is linked to the MiniSat SAT solver. 
c *** See http://minisat.se/MiniSat.html
c *** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
c *** Copyright (c) 2007-2010, Niklas Sorensson
c 
c -- no counterexample found with bound 0
c -- no counterexample found with bound 1
c -- no counterexample found with bound 2
c -- no counterexample found with bound 3
c -- no counterexample found with bound 4
c -- no counterexample found with bound 5
c -- no counterexample found with bound 6
c -- no counterexample found with bound 7
c -- no counterexample found with bound 8
c -- no counterexample found with bound 9
c -- no counterexample found with bound 10
c -- no counterexample found with bound 11
c -- specification  G ((state.token[1] = v1 & state.token[2] = v8) ->  G !((state.token[1] = v7 | state.token[1] = v13) & (state.token[2] = v7 | state.token[2] = v13)))    is false
c -- as demonstrated by the following execution sequence
c Trace Description: BMC Counterexample 
c Trace Type: Counterexample 
c   -> State: 1.1 <-
c     state.token[1] = 0ud8_180
c     state.token[2] = 0ud8_72
c     state.tid = 1
c     state.vid = 2
c     state.target = 0ud8_0
c     v13 = 0ud8_192
c     v12 = 0ud8_80
c     v11 = 0ud8_69
c     v10 = 0ud8_100
c     v9 = 0ud8_98
c     v8 = 0ud8_72
c     v7 = 0ud8_60
c     v6 = 0ud8_44
c     v5 = 0ud8_168
c     v4 = 0ud8_154
c     v3 = 0ud8_153
c     v2 = 0ud8_148
c     v1 = 0ud8_180
c     v0 = 0ud8_0
c   -> State: 1.2 <-
c     state.vid = 9
c     state.target = 0ud8_148
c   -> State: 1.3 <-
c     state.token[1] = 0ud8_148
c     state.tid = 2
c     state.vid = 3
c     state.target = 0ud8_98
c   -> State: 1.4 <-
c     state.token[2] = 0ud8_98
c     state.tid = 1
c     state.vid = 10
c     state.target = 0ud8_153
c   -> State: 1.5 <-
c     state.token[1] = 0ud8_153
c     state.tid = 2
c     state.vid = 4
c     state.target = 0ud8_100
c   -> State: 1.6 <-
c     state.token[2] = 0ud8_100
c     state.tid = 1
c     state.vid = 11
c     state.target = 0ud8_154
c   -> State: 1.7 <-
c     state.token[1] = 0ud8_154
c     state.tid = 2
c     state.vid = 5
c     state.target = 0ud8_69
c   -> State: 1.8 <-
c     state.token[2] = 0ud8_69
c     state.tid = 1
c     state.vid = 12
c     state.target = 0ud8_168
c   -> State: 1.9 <-
c     state.token[1] = 0ud8_168
c     state.tid = 2
c     state.vid = 6
c     state.target = 0ud8_80
c   -> State: 1.10 <-
c     state.token[2] = 0ud8_80
c     state.tid = 1
c     state.vid = 13
c     state.target = 0ud8_44
c   -> State: 1.11 <-
c     state.token[1] = 0ud8_44
c     state.tid = 2
c     state.vid = 7
c     state.target = 0ud8_192
c   -> State: 1.12 <-
c     state.token[2] = 0ud8_192
c     state.tid = 1
c     state.vid = 12
c     state.target = 0ud8_60
c   -> State: 1.13 <-
c     state.token[1] = 0ud8_60
c     state.vid = 1
c     state.target = 0ud8_80
s 1 8
t 7 13
a YES
a 1 8
a 2 8
a 2 9
a 3 9
a 3 10
a 4 10
a 4 11
a 5 11
a 5 12
a 6 12
a 6 13
a 7 13