------------------------------ MODULE amstrong ------------------------------
EXTENDS TLC, Integers, Naturals
CONSTANT n

(*
--algorithm System{
variables sum=0, temp, remainder, digits=0;
{
    chk1:temp:=n;
\* Count number of digits
    chk0:while(temp # 0) {
        digits:=digits+1;
        temp := temp \div 10 ;
    };
    temp := n ;
    chk2:while ( temp # 0 ) {
        remainder := temp%10;
        chk3:sum := sum + remainder^digits ;
        temp := temp \div 10 ;
    };
    if ( n = sum )
        print <<"is an Armstrong number.\n " >>
    else
        print <<" is not an Armstrong number.\n">>
    }
}
*)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES sum, temp, remainder, digits, pc

vars == << sum, temp, remainder, digits, pc >>

Init == (* Global variables *)
        /\ sum = 0
        /\ temp = defaultInitValue
        /\ remainder = defaultInitValue
        /\ digits = 0
        /\ pc = "chk1"

chk1 == /\ pc = "chk1"
        /\ temp' = n
        /\ pc' = "chk0"
        /\ UNCHANGED << sum, remainder, digits >>

chk0 == /\ pc = "chk0"
        /\ IF temp # 0
              THEN /\ digits' = digits+1
                   /\ temp' = (temp \div 10)
                   /\ pc' = "chk0"
              ELSE /\ temp' = n
                   /\ pc' = "chk2"
                   /\ UNCHANGED digits
        /\ UNCHANGED << sum, remainder >>

chk2 == /\ pc = "chk2"
        /\ IF temp # 0
              THEN /\ remainder' = temp%10
                   /\ pc' = "chk3"
              ELSE /\ IF n = sum
                         THEN /\ PrintT(<<"is an Armstrong number.\n " >>)
                         ELSE /\ PrintT(<<" is not an Armstrong number.\n">>)
                   /\ pc' = "Done"
                   /\ UNCHANGED remainder
        /\ UNCHANGED << sum, temp, digits >>

chk3 == /\ pc = "chk3"
        /\ sum' = sum + remainder^digits
        /\ temp' = (temp \div 10)
        /\ pc' = "chk2"
        /\ UNCHANGED << remainder, digits >>

Next == chk1 \/ chk0 \/ chk2 \/ chk3
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

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

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

\* END TRANSLATION


Qerr == pc = "chk3" /\ sum < 2147483647
Qpc == (pc = "Done") => sum >= n

=============================================================================
\* Modification History
\* Last modified Fri May 27 14:46:12 CEST 2016 by arthur
\* Created Fri May 27 14:40:23 CEST 2016 by arthur