Guessed query file: ../../../infof410_goat/INFOF410_SAS_modelv2.q
Options for the verification:
  Generating no trace
  Search order is breadth first (UPPAAL), automatic (TIGA)
  Using conservative space optimisation
  Seed is 1401456426
  State space representation uses minimal constraint systems

Verifying property 1 at line 6
 -- Property is satisfied.

Verifying property 2 at line 11
 -- Property is NOT satisfied.

Verifying property 3 at line 16
 -- Property is NOT satisfied.

Verifying property 4 at line 21
 -- Property is satisfied.

Verifying property 5 at line 28
Preparing: 0%Preparing: 1%Preparing: 2%Preparing: 3%Preparing: 4%Preparing: 5%Preparing: 6%Preparing: 7%Preparing: 8%Preparing: 9%Preparing: 10%Preparing: 11%Preparing: 12%Preparing: 13%Preparing: 14%Preparing: 15%Preparing: 16%Preparing: 17%Preparing: 18%Preparing: 19%Preparing: 20%Preparing: 21%Preparing: 22%Preparing: 23%Preparing: 24%Preparing: 25%Preparing: 26%Preparing: 27%Preparing: 28%Preparing: 29%Preparing: 30%Preparing: 31%Preparing: 32%Preparing: 33%Preparing: 34%Preparing: 35%Preparing: 36%Preparing: 37%Preparing: 38%Preparing: 39%Preparing: 40%Preparing: 41%Preparing: 42%Preparing: 43%Preparing: 44%Preparing: 45%Preparing: 46%Preparing: 47%Preparing: 48%Preparing: 49%Preparing: 50%Preparing: 51%Preparing: 52%Preparing: 53%Preparing: 54%Preparing: 55%Preparing: 56%Preparing: 57%Preparing: 58%Preparing: 59%Preparing: 60%Preparing: 61%Preparing: 62%Preparing: 63%Preparing: 64%Preparing: 65%Preparing: 66%Preparing: 67%Preparing: 68%Preparing: 69%Preparing: 70%Preparing: 71%Preparing: 72%Preparing: 73%Preparing: 74%Preparing: 75%Preparing: 76%Preparing: 77%Preparing: 78%Preparing: 79%Preparing: 80%Preparing: 81%Preparing: 82%Preparing: 83%Preparing: 84%Preparing: 85%Preparing: 86%Preparing: 87%Preparing: 88%Preparing: 89%Preparing: 90%Preparing: 91%Preparing: 92%Preparing: 93%Preparing: 94%Preparing: 95%Preparing: 96%Preparing: 97%Preparing: 98%Preparing: 99% -- Property is satisfied.
$v_gameInfoPlayInitial state:
( User.before_sas Sas.idle ) gateConf=1 
(timeInSas==User.x && User.x==Sas.x && Sas.x==0)

Strategy to avoid losing:

	State: ( User.in_sas Sas.process_card ) gateConf=0 
	When you are in (timeInSas<=10), take transition Sas.process_card->Sas.handling_user { 1, tau, gateConf := 2 }

	State: ( User.in_sas Sas.handling_user ) gateConf=2 
	While you are in	(timeInSas<=10), wait.

	State: ( User.in_sas Sas.handling_user ) gateConf=0 
	While you are in	(timeInSas<=10), wait.

	State: ( User.before_sas Sas.idle ) gateConf=1 
	While you are in	true, wait.

	State: ( User.in_sas Sas.process_card ) gateConf=2 
	When you are in (timeInSas<=10), take transition Sas.process_card->Sas.handling_user { 1, tau, gateConf := 2 }

	State: ( User.after_sas Sas.idle ) gateConf=1 
	While you are in	true, wait.

Verifying property 6 at line 33
 -- Property is satisfied.