%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% The Terma model as in Tomas and Theo %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Initial Parameters %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% rew PROCESSING_TIME=11 % tPERSONALYZE. % If the station is idle, its time is 0, after it lifted the card, its time becomes 1, % then with each tick it increases till it becomes PROCESSING_TIME LOADING_TIME=3 % tLOAD=tUNLOAD. See above MAX_PROGRAM=38 % NCARDS (min 1) (0 is the empty conveyer cell, 1..MAX_PROGRAM are the cards to process % (MAX_PROGRAM in total),MAX_PROGRAM+1..2*MAXPROGRAM are the processed cards) MAX_STATION=4 % NPERS (0 is the unloading point, 1..MAX_STATION are pers stations, % MAX_STATION+1 is the loading point) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Initial Parameter Declarations %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% map PROCESSING_TIME:->Nat LOADING_TIME:->Nat MAX_PROGRAM:->Nat MAX_STATION:->Nat CONVEYER_SIZE:->Nat % NPERS+2 rew CONVEYER_SIZE=succ(succ(MAX_STATION)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% sort Bool (Booleans) %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sort Bool func T,F: -> Bool map and: Bool#Bool -> Bool or: Bool#Bool -> Bool not: Bool -> Bool if: Bool#Bool#Bool -> Bool eq: Bool#Bool -> Bool gt: Bool#Bool -> Bool var b,b1,b2: Bool rew and(T,b)=b and(b,T)=b and(b,F)=F and(F,b)=F and(b,b)=b and(b,not(b))=F and(not(b),b)=F and(or(b,b1),b2)=or(and(b,b2),and(b1,b2)) and(b,or(b1,b2))=or(and(b,b1),and(b,b2)) or(T,b)=T or(b,T)=T or(b,F)=b or(F,b)=b or(b,b)=b or(b,not(b))=T or(not(b),b)=T not(F)=T not(T)=F not(not(b))=b not(or(b,b1))=and(not(b),not(b1)) not(and(b,b1))=or(not(b),not(b1)) if(T,b1,b2)=b1 if(F,b1,b2)=b2 if(b,b1,b1)=b1 if(not(b),b1,b2)=if(b,b2,b1) if(b,T,b2)=or(b,b2) if(b,F,b2)=and(not(b),b2) if(b,b1,T)=or(not(b),b1) if(b,b1,F)=and(b,b1) if(b,b1,b2)=or(or(and(b,b1),and(not(b),b2)),and(b1,b2)) eq(b,b)=T eq(b,not(b))=F eq(not(b),b)=F eq(not(b),not(b1))=eq(b,b1) eq(F,b)=not(b) eq(b,F)=not(b) eq(T,b)=b eq(b,T)=b eq(b,b1)=or(and(b,b1),and(not(b),not(b1))) gt(b,b)=F gt(T,F)=T gt(b,T)=F %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% sort Nat (Natural numbers with binary representations) %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sort Nat func 0: -> Nat x2p1: Nat -> Nat % 2n+1 x2p2: Nat -> Nat % 2n+2 map eq: Nat#Nat -> Bool 1,2,3,4,5,6,7,8,9,10,11,12,13,14, 15,16,17,18,19,20,21,22,23,24,25, 26,27,28,29,30,31,32,33,34,35,36, 37,38: -> Nat % useful abbreviations x2p0: Nat -> Nat % 2n succ: Nat -> Nat % n+1 pred: Nat -> Nat % n-1 gt: Nat#Nat -> Bool % greater than if: Bool#Nat#Nat -> Nat add,sub,csub: Nat#Nat -> Nat % addition, subtraction (partial), cut-off subtraction divides: Nat#Nat -> Bool % does the first argument divide the second? (partial) var n,m: Nat b:Bool rew gt(n,n)=F gt(0,n)=F gt(x2p1(n),0)=T gt(x2p2(n),0)=T gt(x2p1(n),x2p2(m))=gt(n,m) gt(x2p2(n),x2p1(m))=not(gt(m,n)) gt(x2p1(n),x2p1(m))=gt(n,m) gt(x2p2(n),x2p2(m))=gt(n,m) % eq(n,m)=not(or(gt(n,m),gt(m,n))) % sane, but inefficient eq(n,n)=T eq(x2p1(n),0)=F eq(0,x2p1(n))=F eq(x2p2(n),0)=F eq(0,x2p2(n))=F eq(x2p1(n),x2p2(m))=F eq(x2p2(n),x2p1(m))=F eq(x2p2(n),x2p2(m))=eq(n,m) eq(x2p1(n),x2p1(m))=eq(n,m) 1=x2p1(0) 2=x2p2(0) % 1=2*0+1 2=2*0+2 3=x2p1(1) 4=x2p2(1) % 3=2*1+1 4=2*1+2 5=x2p1(2) 6=x2p2(2) % 5=2*2+1 6=2*2+2 7=x2p1(3) 8=x2p2(3) 9=x2p1(4) 10=x2p2(4) 11=x2p1(5) 12=x2p2(5) 13=x2p1(6) 14=x2p2(6) 15=x2p1(7) 16=x2p2(7) 17=x2p1(8) 18=x2p2(8) 19=x2p1(9) 20=x2p2(9) 21=x2p1(10) 22=x2p2(10) 23=x2p1(11) 24=x2p2(11) 25=x2p1(12) 26=x2p2(12) 27=x2p1(13) 28=x2p2(13) 29=x2p1(14) 30=x2p2(14) 31=x2p1(15) 32=x2p2(15) 33=x2p1(16) 34=x2p2(16) 35=x2p1(17) 36=x2p2(17) 37=x2p1(18) 38=x2p2(18) x2p0(0)=0 % 2*0=0 x2p0(x2p1(n))=x2p2(x2p0(n)) % 2(2n+1)=2(2n)+2 x2p0(x2p2(n))=x2p2(x2p1(n)) % 2(2n+2)=2((2n+1)+1)=2(2n+1)+2 succ(0)=x2p1(0) % 0+1=2*0+1 succ(x2p1(n))=x2p2(n) % (2n+1)+1=2n+2 succ(x2p2(n))=x2p1(succ(n)) % (2n+2)+1=2(n+1)+1 % pred(0)=undef pred(x2p1(n))=x2p0(n) % (2n+1)-1=2n pred(x2p2(n))=x2p1(n) % (2n+2)-1=2n+1 add(0,n)=n add(n,0)=n add(x2p1(n),x2p1(m))=x2p2(add(n,m)) % (2n+1)+(2m+1)=2(n+m)+2 add(x2p2(n),x2p2(m))=x2p2(succ(add(n,m))) % (2n+2)+(2m+2)=2(n+m)+4=2(n+m+1)+2 add(x2p1(n),x2p2(m))=x2p1(succ(add(n,m))) % (2n+1)+(2m+2)=2(n+m)+3=2(n+m+1)+1 add(x2p2(n),x2p1(m))=x2p1(succ(add(n,m))) % (2n+2)+(2m+1)=2(n+m)+3=2(n+m+1)+1 sub(n,0)=n sub(n,n)=0 % sub(0,x2p{1,2}) is undefined sub(x2p1(n),x2p1(m))=x2p0(sub(n,m)) % (2n+1)-(2m+1)=2(n-m) sub(x2p2(n),x2p2(m))=x2p0(sub(n,m)) % (2n+2)-(2m+2)=the same sub(x2p1(n),x2p2(m))=x2p1(sub(n,succ(m))) % (2n+1)-(2m+2)=2(n-m)-1=2(n-(m+1))+1 -- % undefined if n=m! sub(x2p2(n),x2p1(m))=x2p1(sub(n,m)) % (2n+2)-(2m+1)=2(n-m)+1 csub(n,m)=if(gt(n,m),sub(n,m),0) divides(x2p1(n),0)=T divides(x2p2(n),0)=T % any n>0 divides 0; divides(0,n) is undef. divides(x2p1(n),x2p1(m))= % n divides m whenever it divides m-n and(not(gt(n,m)),divides(x2p1(n),sub(x2p1(m),x2p1(n)))) divides(x2p1(n),x2p2(m))= and(not(gt(n,m)),divides(x2p1(n),sub(x2p2(m),x2p1(n)))) divides(x2p2(n),x2p1(m))=F % even never divides odd. divides(x2p2(n),x2p2(m))=divides(succ(n),succ(m)) % (2n+2)|(2m+2) iff (n+1)|(m+1) if(T,n,m)=n if(F,n,m)=m if(b,n,n)=n if(not(b),n,m)=if(b,m,n) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% sort LNat (list of Naturals) %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sort LNat func LNat0:->LNat add:Nat#LNat->LNat map eq:LNat#LNat->Bool if:Bool#LNat#LNat->LNat len:LNat->Nat cat:LNat#LNat->LNat head:LNat->Nat % return the head of the list tail:LNat->LNat in:Nat#LNat->Bool lower:LNat#Nat->LNat % return a sublist containing elems LNat % return a sublist containing elems >=n sub:LNat#Nat->LNat % subtract n from each elem. is_unique:LNat->Bool % are all the elems different? is_sorted:LNat->Bool % is the list sorted? is_each_lower:Nat#LNat->Bool % is each of the elems lower than the first arg? gen0Mm1:Nat->LNat % generate list 0..M-1 (if M=0 then return LNat0) var lnat,lnat1:LNat n,m:Nat b:Bool rew eq(lnat,lnat)=T eq(LNat0,add(n,lnat))=F eq(add(n,lnat),LNat0)=F eq(add(n,lnat),add(m,lnat1))=and(eq(n,m),eq(lnat,lnat1)) if(T,lnat,lnat1)=lnat if(F,lnat,lnat1)=lnat1 if(b,lnat,lnat)=lnat if(not(b),lnat,lnat1)=if(b,lnat1,lnat) len(LNat0)=0 len(add(n,lnat))=succ(len(lnat)) cat(LNat0,lnat)=lnat cat(lnat,LNat0)=lnat cat(add(n,lnat),lnat1)=add(n,cat(lnat,lnat1)) head(add(n,lnat))=n tail(add(n,lnat))=lnat in(n,LNat0)=F in(n,add(m,lnat))=or(eq(n,m),in(n,lnat)) lower(LNat0,n)=LNat0 lower(add(m,lnat),n)=if(gt(n,m),add(m,lower(lnat,n)),lower(lnat,n)) upper(LNat0,n)=LNat0 upper(add(m,lnat),n)=if(gt(n,m),upper(lnat,n),add(m,upper(lnat,n))) sub(LNat0,n)=LNat0 sub(add(m,lnat),n)=add(sub(m,n),sub(lnat,n)) is_unique(LNat0)=T is_unique(add(n,lnat))=and(in(n,lnat),is_unique(lnat)) is_sorted(LNat0)=T is_sorted(add(n,LNat0))=T is_sorted(add(n,add(m,lnat)))=and(not(gt(n,m)),is_sorted(add(m,lnat))) is_each_lower(n,LNat0)=T is_each_lower(n,add(m,lnat))=and(gt(n,m),is_each_lower(n,lnat)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% ANN (Nat array with Nat indices) %%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sort ANN func ANN0 : ->ANN % Array of zeros add : Nat#ANN ->ANN % list of the first elements left->right map eq : ANN#ANN ->Bool if : Bool#ANN#ANN->ANN gt : ANN#ANN ->Bool % lexicographic upd : Nat#Nat#ANN ->ANN % a[n]:=m acc : Nat#ANN ->Nat % a[n] shiftr1: Nat#ANN ->ANN % 0..n-1 -> 1..n a[0]:=0 unique_from : Nat#ANN->Bool % all elements >=n are unique in a rem : Nat#ANN ->ANN % removes n-th element in : Nat#ANN ->Bool % is n in a? (trailing 0s are not in) reduce1 : ANN ->ANN % reduce all non-zero elems by 1. in_or_lower : Nat#ANN ->Bool % is an element >=n in a? (trailing 0s are not in) can_drop : Nat#Nat#ANN ->Bool % can the unit drop the card m at n? var n,m,n1:Nat ann,ann1:ANN b:Bool rew eq(ann,ann)=T eq(ANN0,add(n,ann))=F eq(add(n,ann),ANN0)=F eq(add(n,ann),add(m,ann1))=and(eq(n,m),eq(ann,ann1)) if(T,ann,ann1)=ann if(F,ann,ann1)=ann1 if(b,ann,ann)=ann if(not(b),ann,ann1)=if(b,ann1,ann) upd(n,0,ANN0)=ANN0 upd(0,x2p1(m),ANN0)=add(x2p1(m),ANN0) upd(0,x2p2(m),ANN0)=add(x2p2(m),ANN0) upd(x2p1(n),x2p1(m),ANN0)=add(0,upd(x2p0(n),x2p1(m),ANN0)) upd(x2p1(n),x2p2(m),ANN0)=add(0,upd(x2p0(n),x2p2(m),ANN0)) upd(x2p2(n),x2p1(m),ANN0)=add(0,upd(x2p1(n),x2p1(m),ANN0)) upd(x2p2(n),x2p2(m),ANN0)=add(0,upd(x2p1(n),x2p2(m),ANN0)) upd(0,0,add(n,ANN0))=ANN0 upd(0,0,add(n,add(m,ann)))=add(0,add(m,ann)) upd(0,x2p1(m),add(n,ann))=add(x2p1(m),ann) upd(0,x2p2(m),add(n,ann))=add(x2p2(m),ann) upd(x2p1(n),0,add(0,ann))= if(eq(upd(x2p0(n),0,ann),ANN0),ANN0,add(0,upd(x2p0(n),0,ann))) upd(x2p2(n),0,add(0,ann))= if(eq(upd(x2p1(n),0,ann),ANN0),ANN0,add(0,upd(x2p1(n),0,ann))) upd(x2p1(n),0,add(x2p1(m),ann))=add(x2p1(m),upd(x2p0(n),0,ann)) upd(x2p1(n),0,add(x2p2(m),ann))=add(x2p2(m),upd(x2p0(n),0,ann)) upd(x2p2(n),0,add(x2p1(m),ann))=add(x2p1(m),upd(x2p1(n),0,ann)) upd(x2p2(n),0,add(x2p2(m),ann))=add(x2p2(m),upd(x2p1(n),0,ann)) upd(x2p1(n),x2p1(m),add(n1,ann))=add(n1,upd(x2p0(n),x2p1(m),ann)) upd(x2p2(n),x2p1(m),add(n1,ann))=add(n1,upd(x2p1(n),x2p1(m),ann)) upd(x2p1(n),x2p2(m),add(n1,ann))=add(n1,upd(x2p0(n),x2p2(m),ann)) upd(x2p2(n),x2p2(m),add(n1,ann))=add(n1,upd(x2p1(n),x2p2(m),ann)) acc(n,ANN0)=0 acc(0,add(m,ann))=m acc(x2p1(n),add(m,ann))=acc(x2p0(n),ann) acc(x2p2(n),add(m,ann))=acc(x2p1(n),ann) shiftr1(n,ANN0)=ANN0 shiftr1(0,ann)=ann shiftr1(x2p1(n),add(m,ann))=rem(x2p2(n),add(0,add(m,ann))) shiftr1(x2p2(n),add(m,ann))=rem(succ(x2p2(n)),add(0,add(m,ann))) rem(n,ANN0)=ANN0 rem(0,add(m,ann))=ann rem(x2p1(n),add(0,ann))= if(eq(rem(x2p0(n),ann),ANN0),ANN0,add(0,rem(x2p0(n),ann))) rem(x2p2(n),add(0,ann))= if(eq(rem(x2p1(n),ann),ANN0),ANN0,add(0,rem(x2p1(n),ann))) rem(x2p1(n),add(x2p1(m),ann))=add(x2p1(m),rem(x2p0(n),ann)) rem(x2p2(n),add(x2p1(m),ann))=add(x2p1(m),rem(x2p1(n),ann)) rem(x2p1(n),add(x2p2(m),ann))=add(x2p2(m),rem(x2p0(n),ann)) rem(x2p2(n),add(x2p2(m),ann))=add(x2p2(m),rem(x2p1(n),ann)) unique_from(n,ANN0)=T unique_from(n,add(m,ann))=or(gt(n,m),not(in(m,ann))) in(n,ANN0)=F in(n,add(m,ann))=or(eq(n,m),in(n,ann)) reduce1(ANN0)=ANN0 reduce1(add(0,ann))=add(0,reduce1(ann)) reduce1(add(x2p1(n),ann))=add(x2p0(n),reduce1(ann)) reduce1(add(x2p2(n),ann))=add(x2p1(n),reduce1(ann)) in_or_lower(n,ANN0)=F in_or_lower(n,add(m,ann))=or(not(gt(n,m)),in_or_lower(n,ann)) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% This Function is true if dropping a card by the personalization station makes sense.%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% can_drop(n,m,ANN0)=T can_drop(0,m,add(0,ann))=not(in_or_lower(m,ann)) can_drop(0,m,add(x2p1(n1),ann))=F can_drop(0,m,add(x2p2(n1),ann))=F can_drop(x2p1(n),m,add(n1,ann))=and(or(gt(succ(MAX_PROGRAM),n1),gt(n1,m)),can_drop(x2p0(n),m,ann)) can_drop(x2p2(n),m,add(n1,ann))=and(or(gt(succ(MAX_PROGRAM),n1),gt(n1,m)),can_drop(x2p1(n),m,ann)) act tick __tick reduce __reduce drop,_drop,__drop:Nat#Nat pick,_pick,__pick:Nat#Nat _shift _error _done unlock _unlock __unlock load,_load,__load:Nat unload,_unload,__unload:Nat comm tick|tick=__tick reduce|reduce=__reduce drop|_drop=__drop pick|_pick=__pick unlock|_unlock=__unlock load|_load=__load unload|_unload=__unload proc Conveyer(belt:ANN,locks:Nat,expected_card:Nat)= unlock.Conveyer(belt,pred(locks),expected_card)<|gt(locks,0)|>delta % locked conveyer cannot move. + sum(card:Nat,unload(card).Conveyer(upd(0,card,belt),succ(locks),expected_card))<|eq(acc(0,belt),0)|>delta + sum(station:Nat, pick(station,acc(station,belt)).Conveyer(upd(station,0,belt),locks,expected_card) <|and(gt(acc(station,belt),0),gt(succ(MAX_PROGRAM),acc(station,belt)))|>delta) + sum(station:Nat, sum(program:Nat, drop(station,program). Conveyer(upd(station,program,belt),locks,expected_card) % <|eq(acc(station,belt),0)|>delta)) <|can_drop(station,program,belt)|>delta)) + _load(acc(pred(CONVEYER_SIZE),belt)).reduce. Conveyer(reduce1(upd(pred(CONVEYER_SIZE),0,belt)),succ(locks),expected_card) <|eq(acc(pred(CONVEYER_SIZE),belt),expected_card)|>delta + (tick.( ( Conveyer(shiftr1(pred(CONVEYER_SIZE),belt),locks,expected_card) <|or(eq(acc(pred(pred(CONVEYER_SIZE)),belt),0), eq(acc(pred(pred(CONVEYER_SIZE)),belt),expected_card))|> Error ) <|eq(locks,0)|> Conveyer(belt,locks,expected_card) ) <|or(gt(succ(add(MAX_PROGRAM,MAX_PROGRAM)),expected_card),gt(locks,0))|> _done.delta )<|eq(acc(pred(CONVEYER_SIZE),belt),0)|>delta Error=_error.Error Station(cell:Nat,card:Nat,wait:Nat)= sum(new_card:Nat,_pick(cell,new_card).Station(cell,new_card,1)<|eq(wait,0)|>delta) + _drop(cell,add(MAX_PROGRAM,card)).Station(cell,0,0)<|eq(wait,PROCESSING_TIME)|>delta + tick. ( Station(cell,card,succ(wait)) <|and(gt(wait,0),gt(PROCESSING_TIME,wait))|> Station(cell,card,wait) ) + reduce.( Station(cell,pred(card),wait) <|gt(card,0)|> Station(cell,card,wait) ) UnLoader(current_card:Nat,wait:Nat)= _unload(current_card).UnLoader(succ(current_card),1) <|and(eq(wait,0),gt(succ(MAX_PROGRAM),current_card))|>delta + _unlock.UnLoader(current_card,0)<|eq(LOADING_TIME,wait)|>delta + tick.( UnLoader(current_card,succ(wait)) <|gt(wait,0)|> UnLoader(current_card,wait) )<|gt(LOADING_TIME,wait)|>delta + reduce.UnLoader(pred(current_card),wait) Loader(wait:Nat)= sum(card:Nat,load(card).Loader(1))<|eq(wait,0)|>delta + _unlock.Loader(0)<|eq(LOADING_TIME,wait)|>delta + tick.( Loader(succ(wait)) <|gt(wait,0)|> Loader(wait) )<|gt(LOADING_TIME,wait)|>delta + reduce.Loader(wait) System= hide({__unlock}, encap({tick,reduce,_drop,drop,_pick,pick,unlock,_unlock,load,_load,unload,_unload}, Conveyer(ANN0,0,succ(MAX_PROGRAM)) ||rename({__tick->tick,__reduce->reduce},encap({tick,reduce},UnLoader(1,0) ||rename({__tick->tick,__reduce->reduce},encap({tick,reduce},Loader(0) ||rename({__tick->tick,__reduce->reduce},encap({tick,reduce},Station(4,0,0) ||rename({__tick->tick,__reduce->reduce},encap({tick,reduce},Station(3,0,0) ||rename({__tick->tick,__reduce->reduce},encap({tick,reduce},Station(2,0,0) ||Station(1,0,0) )) )) )) )) )) ) ) init System