5 filósofos

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Standard priorities
 val P_HIGH = 100;
 val P_HIGH = 100;
 
 val P_NORMAL = 1000;
 val P_NORMAL = 1000;
 
 val P_LOW = 10000;
 val P_LOW = 10000;
 
 
 
 Standard declarations
 
 UNIT_t
 
 
 colset UNIT_t = unit timed;
 
 
 
 UNIT_t
 
 ut
 var ut: UNIT_t;
 
 
 UNIT
 
 colset UNIT = unit;
 
 
 F
 
 1
 5
 f
 
 colset F= index f with 1..5;
 
 
 P
 
 1
 5
 p
 
 colset P = index p with 1..5;
 
 fun palitos (f(i)) = 1` p(i) ++ 1` p(if i=5 then 1 else i+1);
 fun palitos (f(i)) = 1` p(i) ++ 1` p(if i=5 then 1 else i+1);
 
 
 
 F
 
 ff
 var ff: F;
 
 
 BOOL
 
 
 
 INT
 
 
 
 
 INT
 
 z
 y
 var z,y: INT;
 
 
 
 INT
 
 u
 var u: INT;
 
 
 INTINF
 
 colset INTINF = intinf;
 
 
 TIME
 
 colset TIME = time;
 
 
 REAL
 
 colset REAL = real;
 
 
 STRING
 
 
 
 
 Ut
 
 t
 var t: Ut;
 
 fun expTime (media: int) =
let
 val MediaReal = Real.fromInt media
 val MR = exponencial ((1.0/MediaReal))
in
 floor (MR)
end;
 fun expTime (media: int) =
let
 val MediaReal = Real.fromInt media
 val MR = exponencial ((1.0/MediaReal))
in
 floor (MR)
end;
 
 var procTime : INT
 
 
 
 
 
 
 
 
 
 Filosofos
 
 
 
 
 
 
 
 
 
 
 F
 
 
 
 
 
 
 F.all()
 
 
 
 
 
 
 
 Palitos
 
 
 
 
 
 
 
 
 
 
 P
 
 
 
 
 
 
 P.all()
 
 
 
 
 
 
 
 Filosofo comendo
 
 
 
 
 
 
 
 
 
 
 F
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 UNIT
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 ff
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 palitos(ff)
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 ff
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 ff
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 palitos(ff)
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 ff
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()
 
 
 
 
 
 
 
 
 
 
 
 p2
 
 
 
 
 
 
 
 
 
 
 UNIT_t
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 p1
 
 
 
 
 
 
 
 
 
 
 UNIT_t
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 UNIT
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 t1
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()@+4
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()@+2
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()
 
 
 
 
 
 
 
 
 
 
 
 p2
UNIT_t
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 p1
 
 
 
 
 
 
 
 
 
 
 UNIT_t
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 UNIT
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 t1
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 t2
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 t3
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()@+4
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()@+2
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 ut
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 ut
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()
 
 
 
 
 
 
 
 
 
 
 
 Numeros
 
 
 
 
 
 
 
 
 
 
 INT
 
 
 
 
 
 
 2`4++
3`5++
4`10
 
 
 
 
 
 
 
 Numeros pares
 
 
 
 
 
 
 
 
 
 
 INT
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 input (u);
output (z,y);
action
(let val par = (u mod 2)=0
in
((if par then u else 0),u+1)
end);
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 u
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 z
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 y
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 Ut
 
 
 
 
 
 
 1`()@28+++
1`()@25+++
1`()@22+++
1`()@19+++
1`()@18+++
1`()@13+++
1`()@8+++
1`()@6+++
1`()@4+++
1`()@3+++
1`()@2+++
1`()@1
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 UNIT
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 input (procTime);
action
(expTime(10));
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 1`()
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 ()@+procTime
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 t
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 <same as model>
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 true
true
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 true
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 false
 
 
 
 
 true
 
 
 
 
 false