------------------------------ MODULE serie6_2 ------------------------------

EXTENDS TLC, Integers, Naturals
CONSTANT n0

=============================================================================
\* Modification History
\* Last modified Mon Nov 23 11:33:08 CET 2015 by arthur
\* Created Mon Nov 23 11:17:14 CET 2015 by arthur

(*
--algorithm resolution{
variables n=n0, reverse=0, rem, temp;
    {   
  l0:temp:=n;
  l1:while(temp # 0)
  {
     rem:=temp % 10;
     reverse:=reverse*10+rem;
     temp:= temp \div 10;
  };
  l2:if(reverse=n)  {
      print <<"%d is a palindrome.",n>>;}
  else
      { print <<"%d is not a palindrome.",n>>; }

    }
}

*)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES n, reverse, rem, temp, pc

vars == << n, reverse, rem, temp, pc >>

Init == (* Global variables *)
        /\ n = defaultInitValue
        /\ reverse = 0
        /\ rem = defaultInitValue
        /\ temp = defaultInitValue
        /\ pc = "l0"

l0 == /\ pc = "l0"
      /\ temp' = n
      /\ pc' = "l1"
      /\ UNCHANGED << n, reverse, rem >>

l1 == /\ pc = "l1"
      /\ IF temp # 0
            THEN /\ rem' = temp % 10
                 /\ reverse' = reverse*10+rem'
                 /\ temp' = (temp \div 10)
                 /\ pc' = "l1"
            ELSE /\ pc' = "l2"
                 /\ UNCHANGED << reverse, rem, temp >>
      /\ n' = n

l2 == /\ pc = "l2"
      /\ IF reverse=n
            THEN /\ PrintT(<<"%d is a palindrome.",n>>)
            ELSE /\ PrintT(<<"%d is not a palindrome.",n>>)
      /\ pc' = "Done"
      /\ UNCHANGED << n, reverse, rem, temp >>

Next == l0 \/ l1 \/ l2
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION