------------------------------- MODULE AddSeq -------------------------------
(***************************************************************************)
(* This module defines the algorithm AddSeq of Figure 6.1 in the book "A   *)
(* Science of Concurrent Program" by Leslie Lamport.  It leaves the values *)
(* of some variables unspecified some states of a behavior.  The module is *)
(* instantiated by the module AddSeq.                                      *)
(***************************************************************************)
EXTENDS Integers, Sequences, TLC

(***************************************************************************)
(* As in the book, DigitSeq is defined to be the set of all nonempty       *)
(* sequences of integers from 0 through 9.  For model checking, TLC must   *)
(* override this definition to let DigitSeq be a finite set of such        *)
(* sequences.                                                              *)
(***************************************************************************)
DigitSeq == Seq(0..9) \ {<< >>}
  
(***************************************************************************)
(* As in the book, Val is defined so that if seq is any element of         *)
(* DigitSeq, then Val(seq) is the value of the number whose decimal        *)
(* representation is the digits of seq in reverse order---for example,     *)
(* Val(<<1,2,3>>) equals 321.  It also defines Val(<< >>)to equal 0.       *)
(***************************************************************************)
RECURSIVE Val(_)
Val(seq) == IF seq = << >> THEN 0 ELSE seq[1] + 10 * Val(Tail(seq))


(***************************************************************************)
(* We define (+) so that Val(s1 (+) s2) equals Val(s1) + Val(s2), for any  *)
(* elements s1 and s2 in DigitSeq.  We do it by recursively defining       *)
(* SAdd(s1, s2, c) to equal Val(s1 (+) s2) + c if s1 and s2 are in         *)
(* DigitSeq and c equals 0 or 1.  The evaluation of SAdd(s1, s2, 0) with   *)
(* this recursive definition is the usual algorithm for adding decimal     *)
(* numbers, where the third argument equals the number "carried".          *)
(* (Remember that the digits are written backwards.)                       *)
(***************************************************************************)
Fix(seq) == IF seq = << >> THEN <<0>> ELSE seq

RECURSIVE SAdd(_,_,_)
SAdd(s1, s2, c) == 
   IF s1 \o s2 = << >>
      THEN IF c=1 THEN <<1>> ELSE << >>
      ELSE LET dig == Fix(s1)[1] + Fix(s2)[1] + c
           IN <<dig % 10>> \o SAdd(Tail(Fix(s1)), Tail(Fix(s2)), dig \div 10)

s1 (+) s2 == SAdd(s1, s2, 0)

(***************************************************************************)
(* Now comes the definition of the algorithm AddSeq.  The operator \div is *)
(* defined in the Integers module so that for any natural numbers m and n  *)
(* with n > 0, the value of m \div n is the largest integer d such that d  *)
(* * n \leq m.                                                             *)
(***************************************************************************)
VARIABLES pc, u, v, sum, carry

vars == << u, v, sum, carry, pc >>

Init == (* Global variables *)
        /\ u \in DigitSeq
        /\ v \in DigitSeq
        /\ sum = << >>
        /\ carry = 0
        /\ pc = "a"

Next == /\ pc = "a"
        /\ IF (u # << >>) \/ (v # << >> \/ carry # 0)
              THEN /\ LET digit == Fix(u)[1] + Fix(v)[1] + carry IN
                        /\ sum' = Append(sum, digit % 10)
                        /\ carry' = (digit \div 10)
                   /\ u' = Tail(Fix(u))
                   /\ v' = Tail(Fix(v))
                   /\ pc' = "a"
              ELSE /\ carry' = 0
                   /\ pc' = "done"
                   /\ UNCHANGED << u, v, sum >>

AddSeq == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
(***************************************************************************)
(* The following asserts that the abstract program AddSeq implements the   *)
(* abstract program Add of module Add under the refinement mapping         *)
(* described in Section 6.1.3.                                             *)
(***************************************************************************)
endBar == sum # << >> 
xBar == IF endBar THEN 0 ELSE Val(u)
yBar == IF endBar THEN 0 ELSE Val(v)
zBar == Val(sum) + (10^Len(sum)) * (carry + Val(u) + Val(v))

A == INSTANCE Add WITH x <- xBar, y <- yBar, end <- endBar, z <- zBar 

THEOREM AddSeq => A!Add
=============================================================================
\* Modification History
\* Last modified Tue Oct 15 15:44:45 CEST 2024 by lamport
\* Created Mon Apr 10 10:43:22 PDT 2023 by lamport
