title: need help in ATM Alloy
body: <p>I am trying to model that, ATM system which provides an available amount of money after authenticates that the card and pin are correct, otherwise,  the amount of money is not provided.
  Also if the card is incorrect, it will be rejected
  if the pin is not correct , it will be rejected</p>
  
  <p>In the first model, there is a counterexample appeared and I fixed it in the second model below.</p>
  
  <p>My question is, I just wonder if my model is fine?
  and solving the counterexample is correct ?
  Thanks</p>
  
  <p>The model with counterexample :</p>
  
  <pre><code>module ATM_Sys
  one sig Enter_Card {}
  abstract sig ATM_Operation {}
  one sig  Reject_Pin, Reject_Card, Provides_Amount,Dont_Provides_Amount extends ATM_Operation{}
  
  
  sig ATM {
  card : lone Card , 
  userOp :  Enter_Card lone -&gt; card, 
  AtmOp:   userOp-&gt; lone ATM_Operation  
  } 
  
  sig Card
  {
  pin : one Int,
  balance: one Int
  }
  
  fact   {all  crd,pn:Card| crd.balance &gt;0 &amp;&amp; pn.pin &gt;0 } 
  
  pred Start[atm,atm':ATM,crd:Card]
  {
  atm.userOp=Enter_Card-&gt;crd &amp;&amp;
  atm'.card=crd &amp;&amp; atm'.card=atm.card &amp;&amp; TypePin [atm,atm']
  }
  
  pred TypePin[atm,atm':ATM]
  {
   atm'.card.pin=Int &amp;&amp; atm'.card.pin=atm.card.pin implies SelectAmount[atm,atm']
  }
  
  pred SelectAmount[atm,atm':ATM]
  {
   atm'.card.balance=Int  implies atm'.AtmOp=atm.userOp-&gt;Provides_Amount
  }
  
  assert ATM_System
  {all atm,atm':ATM,crd:Card|
  Start[atm,atm',crd]  =&gt;( 
  atm'.card!=atm.card  &amp;&amp; atm'.AtmOp=atm.userOp-&gt;Reject_Card ||
  atm'.card.pin!=atm.card.pin &amp;&amp;atm'.AtmOp=atm.userOp-&gt;Reject_Pin || 
  atm'.card.balance!=atm.card.balance  &amp;&amp; atm'.AtmOp=atm.userOp-&gt;Dont_Provides_Amount )
  }
  
  check ATM_System for 1
  run Start 
  </code></pre>
  
  <hr>
  
  <p>The model without counterexample :</p>
  
  <pre><code>module ATM_Sys
  one sig Enter_Card {}
  abstract sig ATM_Operation {}
  one sig  Reject_Pin, Reject_Card, Provides_Amount,Dont_Provides_Amount extends ATM_Operation{}
  
  
  sig ATM {
  card : lone Card , 
  userOp :  Enter_Card lone -&gt; card, 
  AtmOp:   userOp-&gt; lone ATM_Operation  
  } 
  
  sig Card
  {
  pin : one Int,
  balance: one Int
  }
  
  fact   {all  crd,pn:Card| crd.balance &gt;0 &amp;&amp; pn.pin &gt;0 } 
  
  pred Start[atm,atm':ATM,crd:Card]
  {
  atm.userOp=Enter_Card-&gt;crd &amp;&amp;
  atm'.card=crd &amp;&amp; atm'.card=atm.card &amp;&amp; TypePin [atm,atm']
  }
  
  pred TypePin[atm,atm':ATM]
  {
   atm'.card.pin=Int &amp;&amp; atm'.card.pin=atm.card.pin implies SelectAmount[atm,atm']
  }
  
  pred SelectAmount[atm,atm':ATM]
  {
   atm'.card.balance=Int  implies atm'.AtmOp=atm.userOp-&gt;Provides_Amount
  }
  
  assert ATM_System
  {all atm,atm':ATM,crd:Card|
  Start[atm,atm',crd]  =&gt;( 
  atm'.card!=atm.card  =&gt; atm'.AtmOp=atm.userOp-&gt;Reject_Card ||
  atm'.card.pin!=atm.card.pin =&gt;atm'.AtmOp=atm.userOp-&gt;Reject_Pin || 
  atm'.card.balance!=atm.card.balance  =&gt; atm'.AtmOp=atm.userOp-&gt;Dont_Provides_Amount )
  }
  
  check ATM_System for 1
  run Start 
  </code></pre>
  
  <p>Also, when I fixed the counterexample, I noticed that, under any number of 
  scopes, there is still no counterexample . Is that correct ?</p>
  
  <p>Thanks</p>