************************************************************ * IMITATOR 2.8.1-working "Butter Ham" * * * * Etienne Andre, Ulrich Kuehne et al. * * 2009 - 2016 * * LSV, ENS de Cachan & CNRS, France * * LIPN, Universite Paris 13, Sorbonne Paris Cite, France * * www.imitator.fr * * * * Build: 2104 (2016-11-23 15:02:25 UTC) * * learning/5d10a02 * ************************************************************ Analysis time: Wed Dec 7, 2016 16:29:49 Model: /home/gia/Desktop/experiments/Etienne/csmacdPrism/csmacdPrism.imi Mode: parametric non-Zeno emptiness checking (CUB checking). Time elapsing will be applied at the beginning of the computation of a new state. The result will be written to a file. *** Warning: IMITATOR will try to stop after 3600 seconds. Abstract model built after 0.006 second. Memory for abstract model: 1044.875 KiB (i.e., 267488 words) Checking the PTA is CUB for some valuations… The model is a CUB-PTA for the following valuations: False *** Warning: The initial constraint of the model is not satisfiable. IMITATOR successfully terminated (after 0.013 second) Estimated memory used: 2.435 MiB (i.e., 319291 words of size 8)