[0m************************************************************
* [1mIMITATOR 2.10.4 "Butter Jellyfish"[0m *
* *
* Etienne Andre et al. *
* 2009 - 2018 *
* LSV, ENS de Cachan & CNRS, France *
* LIPN, Universite Paris 13, France *
* www.imitator.fr *
* *
* Build: 2477 (2018-07-02 09:42:27 UTC) *
* HEAD/5b53333 *
************************************************************[0m
[0mModel: category4_vulnerable.imi[0m
[0mMode: EFunsafe-synthesis.[0m
[0mConsidering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality).[0m
[0mMerging technique of [AFS13] enabled.[0m
[0mThe result will be written to a file.[0m
[0mStarting running algorithm EFunsafe…
[0m
[0mComputing post^1 from 1 state.[0m
[0mComputing post^2 from 1 state.[0m
[0mComputing post^3 from 1 state.[0m
[0mComputing post^4 from 3 states.[0m
[0mComputing post^5 from 1 state.[0m
[0mComputing post^6 from 10 states.[0m
[0mComputing post^7 from 10 states.[0m
[0mComputing post^8 from 10 states.[0m
[0mComputing post^9 from 10 states.[0m
[0mComputing post^10 from 10 states.[0m
[0mComputing post^11 from 10 states.[0m
[0mComputing post^12 from 10 states.[0m
[0mComputing post^13 from 10 states.[0m
[0mComputing post^14 from 10 states.[0m
[0mComputing post^15 from 10 states.[0m
[0mComputing post^16 from 10 states.[0m
[0mComputing post^17 from 10 states.[0m
[0mComputing post^18 from 10 states.[0m
[0mComputing post^19 from 10 states.[0m
[0mComputing post^20 from 10 states.[0m
[0mComputing post^21 from 10 states.[0m
[0mComputing post^22 from 10 states.[0m
[0mComputing post^23 from 10 states.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m [EFunsafe] Found a new state violating the property.[0m
[0m
Fixpoint reached at a depth of 24: 197 states with 196 transitions in the final state space.[0m
[0m
[EFunsafe] Algorithm completed after 0.259 second.[0m
[0m
Final constraint such that the system is incorrect:[0m
[92;40m abs_ptime >= 5400000
& 5400004 >= abs_ptime
OR
abs_ptime >= 6750000
& 6750004 >= abs_ptime
OR
abs_ptime >= 4050000
& 4050004 >= abs_ptime
OR
abs_ptime >= 8100000
& 8100004 >= abs_ptime
OR
abs_ptime >= 2700000
& 2700004 >= abs_ptime
OR
abs_ptime >= 9450000
& 9450004 >= abs_ptime
OR
abs_ptime >= 1350000
& 1350004 >= abs_ptime
OR
abs_ptime >= 10800000
& 10800004 >= abs_ptime
OR
13500004 >= abs_ptime
& abs_ptime >= 13500000
OR
12150004 >= abs_ptime
& abs_ptime >= 12150000[0m
[94mThis bad constraint is exact (sound and complete)[0m
[0m
Result written to file 'category4_vulnerable.res'.[0m
[0m[1mIMITATOR successfully terminated[0m (after 0.260 second)[0m