Skip to content
GitLab
Commit a975d8f2 authored by FellnerA's avatar FellnerA
Browse files

Add example models

parent 44f5162b
Expand all Hide whitespace changes
Inline Side-by-side
example_models/allpar/allPar_10.ooas 0 → 100644
View file @ a975d8f2
types
t_int = int [0..10];
model = autocons system |[
var
x0 : t_int = 0;
x1 : t_int = 0;
x2 : t_int = 0;
x3 : t_int = 0;
x4 : t_int = 0;
x5 : t_int = 0;
x6 : t_int = 0;
x7 : t_int = 0;
x8 : t_int = 0;
x9 : t_int = 0
actions
obs A0 = requires x0 = 0 : x0 := 1 end;
obs A1 = requires x1 = 0 : x1 := 1 end;
obs A2 = requires x2 = 0 : x2 := 1 end;
obs A3 = requires x3 = 0 : x3 := 1 end;
obs A4 = requires x4 = 0 : x4 := 1 end;
obs A5 = requires x5 = 0 : x5 := 1 end;
obs A6 = requires x6 = 0 : x6 := 1 end;
obs A7 = requires x7 = 0 : x7 := 1 end;
obs A8 = requires x8 = 0 : x8 := 1 end;
obs A9 = requires x9 = 0 : x9 := 1 end;
ctr reset = requires x0 = 1 and x1 = 1 and x2 = 1 and x3 = 1 and x4 = 1 and x5 = 1 and x6 = 1 and x7 = 1 and x8 = 1 and x9 = 1 : x0 := 0; x1 := 0; x2 := 0; x3 := 0; x4 := 0; x5 := 0; x6 := 0; x7 := 0; x8 := 0; x9 := 0 end
do
A0 [] A1 [] A2 [] A3 [] A4 [] A5 [] A6 [] A7 [] A8 [] A9 [] reset
od
]|
system
model
example_models/allpar/allPar_50.ooas 0 → 100644
View file @ a975d8f2
types
t_int = int [0..10];
model = autocons system |[
var
x0 : t_int = 0;
x1 : t_int = 0;
x2 : t_int = 0;
x3 : t_int = 0;
x4 : t_int = 0;
x5 : t_int = 0;
x6 : t_int = 0;
x7 : t_int = 0;
x8 : t_int = 0;
x9 : t_int = 0;
x10 : t_int = 0;
x11 : t_int = 0;
x12 : t_int = 0;
x13 : t_int = 0;
x14 : t_int = 0;
x15 : t_int = 0;
x16 : t_int = 0;
x17 : t_int = 0;
x18 : t_int = 0;
x19 : t_int = 0;
x20 : t_int = 0;
x21 : t_int = 0;
x22 : t_int = 0;
x23 : t_int = 0;
x24 : t_int = 0;
x25 : t_int = 0;
x26 : t_int = 0;
x27 : t_int = 0;
x28 : t_int = 0;
x29 : t_int = 0;
x30 : t_int = 0;
x31 : t_int = 0;
x32 : t_int = 0;
x33 : t_int = 0;
x34 : t_int = 0;
x35 : t_int = 0;
x36 : t_int = 0;
x37 : t_int = 0;
x38 : t_int = 0;
x39 : t_int = 0;
x40 : t_int = 0;
x41 : t_int = 0;
x42 : t_int = 0;
x43 : t_int = 0;
x44 : t_int = 0;
x45 : t_int = 0;
x46 : t_int = 0;
x47 : t_int = 0;
x48 : t_int = 0;
x49 : t_int = 0
actions
obs A0 = requires x0 = 0 : x0 := 1 end;
obs A1 = requires x1 = 0 : x1 := 1 end;
obs A2 = requires x2 = 0 : x2 := 1 end;
obs A3 = requires x3 = 0 : x3 := 1 end;
obs A4 = requires x4 = 0 : x4 := 1 end;
obs A5 = requires x5 = 0 : x5 := 1 end;
obs A6 = requires x6 = 0 : x6 := 1 end;
obs A7 = requires x7 = 0 : x7 := 1 end;
obs A8 = requires x8 = 0 : x8 := 1 end;
obs A9 = requires x9 = 0 : x9 := 1 end;
obs A10 = requires x10 = 0 : x10 := 1 end;
obs A11 = requires x11 = 0 : x11 := 1 end;
obs A12 = requires x12 = 0 : x12 := 1 end;
obs A13 = requires x13 = 0 : x13 := 1 end;
obs A14 = requires x14 = 0 : x14 := 1 end;
obs A15 = requires x15 = 0 : x15 := 1 end;
obs A16 = requires x16 = 0 : x16 := 1 end;
obs A17 = requires x17 = 0 : x17 := 1 end;
obs A18 = requires x18 = 0 : x18 := 1 end;
obs A19 = requires x19 = 0 : x19 := 1 end;
obs A20 = requires x20 = 0 : x20 := 1 end;
obs A21 = requires x21 = 0 : x21 := 1 end;
obs A22 = requires x22 = 0 : x22 := 1 end;
obs A23 = requires x23 = 0 : x23 := 1 end;
obs A24 = requires x24 = 0 : x24 := 1 end;
obs A25 = requires x25 = 0 : x25 := 1 end;
obs A26 = requires x26 = 0 : x26 := 1 end;
obs A27 = requires x27 = 0 : x27 := 1 end;
obs A28 = requires x28 = 0 : x28 := 1 end;
obs A29 = requires x29 = 0 : x29 := 1 end;
obs A30 = requires x30 = 0 : x30 := 1 end;
obs A31 = requires x31 = 0 : x31 := 1 end;
obs A32 = requires x32 = 0 : x32 := 1 end;
obs A33 = requires x33 = 0 : x33 := 1 end;
obs A34 = requires x34 = 0 : x34 := 1 end;
obs A35 = requires x35 = 0 : x35 := 1 end;
obs A36 = requires x36 = 0 : x36 := 1 end;
obs A37 = requires x37 = 0 : x37 := 1 end;
obs A38 = requires x38 = 0 : x38 := 1 end;
obs A39 = requires x39 = 0 : x39 := 1 end;
obs A40 = requires x40 = 0 : x40 := 1 end;
obs A41 = requires x41 = 0 : x41 := 1 end;
obs A42 = requires x42 = 0 : x42 := 1 end;
obs A43 = requires x43 = 0 : x43 := 1 end;
obs A44 = requires x44 = 0 : x44 := 1 end;
obs A45 = requires x45 = 0 : x45 := 1 end;
obs A46 = requires x46 = 0 : x46 := 1 end;
obs A47 = requires x47 = 0 : x47 := 1 end;
obs A48 = requires x48 = 0 : x48 := 1 end;
obs A49 = requires x49 = 0 : x49 := 1 end;
ctr reset = requires x0 = 1 and x1 = 1 and x2 = 1 and x3 = 1 and x4 = 1 and x5 = 1 and x6 = 1 and x7 = 1 and x8 = 1 and x9 = 1 and x10 = 1 and x11 = 1 and x12 = 1 and x13 = 1 and x14 = 1 and x15 = 1 and x16 = 1 and x17 = 1 and x18 = 1 and x19 = 1 and x20 = 1 and x21 = 1 and x22 = 1 and x23 = 1 and x24 = 1 and x25 = 1 and x26 = 1 and x27 = 1 and x28 = 1 and x29 = 1 and x30 = 1 and x31 = 1 and x32 = 1 and x33 = 1 and x34 = 1 and x35 = 1 and x36 = 1 and x37 = 1 and x38 = 1 and x39 = 1 and x40 = 1 and x41 = 1 and x42 = 1 and x43 = 1 and x44 = 1 and x45 = 1 and x46 = 1 and x47 = 1 and x48 = 1 and x49 = 1 : x0 := 0; x1 := 0; x2 := 0; x3 := 0; x4 := 0; x5 := 0; x6 := 0; x7 := 0; x8 := 0; x9 := 0; x10 := 0; x11 := 0; x12 := 0; x13 := 0; x14 := 0; x15 := 0; x16 := 0; x17 := 0; x18 := 0; x19 := 0; x20 := 0; x21 := 0; x22 := 0; x23 := 0; x24 := 0; x25 := 0; x26 := 0; x27 := 0; x28 := 0; x29 := 0; x30 := 0; x31 := 0; x32 := 0; x33 := 0; x34 := 0; x35 := 0; x36 := 0; x37 := 0; x38 := 0; x39 := 0; x40 := 0; x41 := 0; x42 := 0; x43 := 0; x44 := 0; x45 := 0; x46 := 0; x47 := 0; x48 := 0; x49 := 0 end
do
A0 [] A1 [] A2 [] A3 [] A4 [] A5 [] A6 [] A7 [] A8 [] A9 [] A10 [] A11 [] A12 [] A13 [] A14 [] A15 [] A16 [] A17 [] A18 [] A19 [] A20 [] A21 [] A22 [] A23 [] A24 [] A25 [] A26 [] A27 [] A28 [] A29 [] A30 [] A31 [] A32 [] A33 [] A34 [] A35 [] A36 [] A37 [] A38 [] A39 [] A40 [] A41 [] A42 [] A43 [] A44 [] A45 [] A46 [] A47 [] A48 [] A49 [] reset
od
]|
system
model
example_models/ccnfs/CCNFS_3.ooas 0 → 100644
View file @ a975d8f2
types
t_int = int [0..10];
model = autocons system |[
var
x0 : t_int = 0;
x1 : t_int = 0;
x2 : t_int = 0
actions
obs A0 = requires x0 = 0 : x0 := 1 end;
obs B0 = requires x0 = 0 : x0 := 2 end;
obs A1 = requires x1 = 0 : x1 := 1 end;
obs B1 = requires x1 = 0 : x1 := 2 end;
obs A2 = requires x2 = 0 : x2 := 1 end;
obs B2 = requires x2 = 0 : x2 := 2 end;
ctr reset = requires x0 > 0 and x1 > 0 and x2 > 0 : x0 := 0; x1 := 0; x2 := 0 end
do
A0 [] B0 [] A1 [] B1 [] A2 [] B2 [] reset
od
]|
system
model
example_models/ccnfs/CCNFS_6.ooas 0 → 100644
View file @ a975d8f2
types
t_int = int [0..10];
model = autocons system |[
var
x0 : t_int = 0;
x1 : t_int = 0;
x2 : t_int = 0;
x3 : t_int = 0;
x4 : t_int = 0;
x5 : t_int = 0
actions
obs A0 = requires x0 = 0 : x0 := 1 end;
obs B0 = requires x0 = 0 : x0 := 2 end;
obs A1 = requires x1 = 0 : x1 := 1 end;
obs B1 = requires x1 = 0 : x1 := 2 end;
obs A2 = requires x2 = 0 : x2 := 1 end;
obs B2 = requires x2 = 0 : x2 := 2 end;
obs A3 = requires x3 = 0 : x3 := 1 end;
obs B3 = requires x3 = 0 : x3 := 2 end;
obs A4 = requires x4 = 0 : x4 := 1 end;
obs B4 = requires x4 = 0 : x4 := 2 end;
obs A5 = requires x5 = 0 : x5 := 1 end;
obs B5 = requires x5 = 0 : x5 := 2 end;
ctr reset = requires x0 > 0 and x1 > 0 and x2 > 0 and x3 > 0 and x4 > 0 and x5 > 0 : x0 := 0; x1 := 0; x2 := 0; x3 := 0; x4 := 0; x5 := 0 end
do
A0 [] B0 [] A1 [] B1 [] A2 [] B2 [] A3 [] B3 [] A4 [] B4 [] A5 [] B5 [] reset
od
]|
system
model
example_models/parallel_sum/parallel_sum_10.ooas 0 → 100644
View file @ a975d8f2
types
t_int = int [0..10000];
t_parsum = int [0..100000];
t_sum = int [0..1000000];
t_index = int [0..100];
__model = autocons system |[
var
parSummer0 : ParSummer0 = new(ParSummer0, "parSummer0");
parSummer1 : ParSummer1 = new(ParSummer1, "parSummer1");
parSummer2 : ParSummer2 = new(ParSummer2, "parSummer2");
parSummer3 : ParSummer3 = new(ParSummer3, "parSummer3");
parSummer4 : ParSummer4 = new(ParSummer4, "parSummer4");
parSummer5 : ParSummer5 = new(ParSummer5, "parSummer5");
parSummer6 : ParSummer6 = new(ParSummer6, "parSummer6");
parSummer7 : ParSummer7 = new(ParSummer7, "parSummer7");
parSummer8 : ParSummer8 = new(ParSummer8, "parSummer8");
parSummer9 : ParSummer9 = new(ParSummer9, "parSummer9");
in_progress: bool = true;
summands : list [100] of t_int = [0, 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, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99];
sum: t_sum = 0
actions
obs total_sum(s : t_int) = requires in_progress and
parSummer0.finished() and
parSummer1.finished() and
parSummer2.finished() and
parSummer3.finished() and
parSummer4.finished() and
parSummer5.finished() and
parSummer6.finished() and
parSummer7.finished() and
parSummer8.finished() and
parSummer9.finished():
in_progress := false
end;
calculate_sum = requires in_progress and
parSummer0.finished() and
parSummer1.finished() and
parSummer2.finished() and
parSummer3.finished() and
parSummer4.finished() and
parSummer5.finished() and
parSummer6.finished() and
parSummer7.finished() and
parSummer8.finished() and
parSummer9.finished() :
sum :=(
parSummer0.getSum() +
parSummer1.getSum() +
parSummer2.getSum() +
parSummer3.getSum() +
parSummer4.getSum() +
parSummer5.getSum() +
parSummer6.getSum() +
parSummer7.getSum() +
parSummer8.getSum() +
parSummer9.getSum())
end;
ctr overflow(s : t_sum) = requires s > 10000: skip end;
ctr assign_chunk0 = requires not parSummer0.finished() :
parSummer0.receive_chunk([summands[0],summands[1],summands[2],summands[3],summands[4],summands[5],summands[6],summands[7],summands[8],summands[9]])
end;
ctr assign_chunk1 = requires not parSummer1.finished() :
parSummer1.receive_chunk([summands[10],summands[11],summands[12],summands[13],summands[14],summands[15],summands[16],summands[17],summands[18],summands[19]])
end;
ctr assign_chunk2 = requires not parSummer2.finished() :
parSummer2.receive_chunk([summands[20],summands[21],summands[22],summands[23],summands[24],summands[25],summands[26],summands[27],summands[28],summands[29]])
end;
ctr assign_chunk3 = requires not parSummer3.finished() :
parSummer3.receive_chunk([summands[30],summands[31],summands[32],summands[33],summands[34],summands[35],summands[36],summands[37],summands[38],summands[39]])
end;
ctr assign_chunk4 = requires not parSummer4.finished() :
parSummer4.receive_chunk([summands[40],summands[41],summands[42],summands[43],summands[44],summands[45],summands[46],summands[47],summands[48],summands[49]])
end;
ctr assign_chunk5 = requires not parSummer5.finished() :
parSummer5.receive_chunk([summands[50],summands[51],summands[52],summands[53],summands[54],summands[55],summands[56],summands[57],summands[58],summands[59]])
end;
ctr assign_chunk6 = requires not parSummer6.finished() :
parSummer6.receive_chunk([summands[60],summands[61],summands[62],summands[63],summands[64],summands[65],summands[66],summands[67],summands[68],summands[69]])
end;
ctr assign_chunk7 = requires not parSummer7.finished() :
parSummer7.receive_chunk([summands[70],summands[71],summands[72],summands[73],summands[74],summands[75],summands[76],summands[77],summands[78],summands[79]])
end;
ctr assign_chunk8 = requires not parSummer8.finished() :
parSummer8.receive_chunk([summands[80],summands[81],summands[82],summands[83],summands[84],summands[85],summands[86],summands[87],summands[88],summands[89]])
end;
ctr assign_chunk9 = requires not parSummer9.finished() :
parSummer9.receive_chunk([summands[90],summands[91],summands[92],summands[93],summands[94],summands[95],summands[96],summands[97],summands[98],summands[99]])
end;
ctr reset = requires not in_progress :
summands := [sum + 0, sum + 1, sum + 2, sum + 3, sum + 4, sum + 5, sum + 6, sum + 7, sum + 8, sum + 9, sum + 10, sum + 11, sum + 12, sum + 13, sum + 14, sum + 15, sum + 16, sum + 17, sum + 18, sum + 19, sum + 20, sum + 21, sum + 22, sum + 23, sum + 24, sum + 25, sum + 26, sum + 27, sum + 28, sum + 29, sum + 30, sum + 31, sum + 32, sum + 33, sum + 34, sum + 35, sum + 36, sum + 37, sum + 38, sum + 39, sum + 40, sum + 41, sum + 42, sum + 43, sum + 44, sum + 45, sum + 46, sum + 47, sum + 48, sum + 49, sum + 50, sum + 51, sum + 52, sum + 53, sum + 54, sum + 55, sum + 56, sum + 57, sum + 58, sum + 59, sum + 60, sum + 61, sum + 62, sum + 63, sum + 64, sum + 65, sum + 66, sum + 67, sum + 68, sum + 69, sum + 70, sum + 71, sum + 72, sum + 73, sum + 74, sum + 75, sum + 76, sum + 77, sum + 78, sum + 79, sum + 80, sum + 81, sum + 82, sum + 83, sum + 84, sum + 85, sum + 86, sum + 87, sum + 88, sum + 89, sum + 90, sum + 91, sum + 92, sum + 93, sum + 94, sum + 95, sum + 96, sum + 97, sum + 98, sum + 99];
in_progress := true;
parSummer0.reset();
parSummer1.reset();
parSummer2.reset();
parSummer3.reset();
parSummer4.reset();
parSummer5.reset();
parSummer6.reset();
parSummer7.reset();
parSummer8.reset();
parSummer9.reset()
end
do
(calculate_sum; (overflow(sum) // total_sum(sum))) []
assign_chunk0 []
assign_chunk1 []
assign_chunk2 []
assign_chunk3 []
assign_chunk4 []
assign_chunk5 []
assign_chunk6 []
assign_chunk7 []
assign_chunk8 []
assign_chunk9 []
reset
od
]|;
ParSummer0 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =
result := not in_progress and sum_index = 10
end;
getSum : t_parsum =
result := sum
end;
reset =
sum_index := 0;
sum := 0
end;
receive_chunk(chunk: list[10] of t_int) =
requires not in_progress :
to_process := chunk;
in_progress := true
end
end
actions
obs plus = requires in_progress and sum_index < 10:
sum := sum + to_process[sum_index];
sum_index := sum_index + 1
end;
obs partial_sum(s : t_int) = requires in_progress and sum_index = 10 :
in_progress := false
end;
ctr overflow(s : t_parsum) = requires s > 10000:
skip
end
do
plus [] (overflow(sum) // partial_sum(sum))
od
]|;
ParSummer1 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =
result := not in_progress and sum_index = 10
end;
getSum : t_parsum =
result := sum
end;
reset =
sum_index := 0;
sum := 0
end;
receive_chunk(chunk: list[10] of t_int) =
requires not in_progress :
to_process := chunk;
in_progress := true
end
end
actions
obs plus = requires in_progress and sum_index < 10:
sum := sum + to_process[sum_index];
sum_index := sum_index + 1
end;
obs partial_sum(s : t_int) = requires in_progress and sum_index = 10 :
in_progress := false
end;
ctr overflow(s : t_parsum) = requires s > 10000:
skip
end
do
plus [] (overflow(sum) // partial_sum(sum))
od
]|;
ParSummer2 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =
result := not in_progress and sum_index = 10
end;
getSum : t_parsum =
result := sum
end;
reset =
sum_index := 0;
sum := 0
end;
receive_chunk(chunk: list[10] of t_int) =
requires not in_progress :
to_process := chunk;
in_progress := true
end
end
actions
obs plus = requires in_progress and sum_index < 10:
sum := sum + to_process[sum_index];
sum_index := sum_index + 1
end;
obs partial_sum(s : t_int) = requires in_progress and sum_index = 10 :
in_progress := false
end;
ctr overflow(s : t_parsum) = requires s > 10000:
skip
end
do
plus [] (overflow(sum) // partial_sum(sum))
od
]|;
ParSummer3 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =
result := not in_progress and sum_index = 10
end;
getSum : t_parsum =
result := sum
end;
reset =
sum_index := 0;
sum := 0
end;
receive_chunk(chunk: list[10] of t_int) =
requires not in_progress :
to_process := chunk;
in_progress := true
end
end
actions
obs plus = requires in_progress and sum_index < 10:
sum := sum + to_process[sum_index];
sum_index := sum_index + 1
end;
obs partial_sum(s : t_int) = requires in_progress and sum_index = 10 :
in_progress := false
end;
ctr overflow(s : t_parsum) = requires s > 10000:
skip
end
do
plus [] (overflow(sum) // partial_sum(sum))
od
]|;
ParSummer4 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =
result := not in_progress and sum_index = 10
end;
getSum : t_parsum =
result := sum
end;
reset =
sum_index := 0;
sum := 0
end;
receive_chunk(chunk: list[10] of t_int) =
requires not in_progress :
to_process := chunk;
in_progress := true
end
end
actions
obs plus = requires in_progress and sum_index < 10:
sum := sum + to_process[sum_index];
sum_index := sum_index + 1
end;
obs partial_sum(s : t_int) = requires in_progress and sum_index = 10 :
in_progress := false
end;
ctr overflow(s : t_parsum) = requires s > 10000:
skip
end
do
plus [] (overflow(sum) // partial_sum(sum))
od
]|;
ParSummer5 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =
result := not in_progress and sum_index = 10
end;
getSum : t_parsum =
result := sum
end;
reset =
sum_index := 0;
sum := 0
end;
receive_chunk(chunk: list[10] of t_int) =
requires not in_progress :
to_process := chunk;
in_progress := true
end
end
actions
obs plus = requires in_progress and sum_index < 10:
sum := sum + to_process[sum_index];
sum_index := sum_index + 1
end;
obs partial_sum(s : t_int) = requires in_progress and sum_index = 10 :
in_progress := false
end;
ctr overflow(s : t_parsum) = requires s > 10000:
skip
end
do
plus [] (overflow(sum) // partial_sum(sum))
od
]|;
ParSummer6 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =
result := not in_progress and sum_index = 10
end;
getSum : t_parsum =
result := sum
end;
reset =
sum_index := 0;
sum := 0
end;
receive_chunk(chunk: list[10] of t_int) =
requires not in_progress :
to_process := chunk;
in_progress := true
end
end
actions
obs plus = requires in_progress and sum_index < 10:
sum := sum + to_process[sum_index];
sum_index := sum_index + 1
end;
obs partial_sum(s : t_int) = requires in_progress and sum_index = 10 :
in_progress := false
end;
ctr overflow(s : t_parsum) = requires s > 10000:
skip
end
do
plus [] (overflow(sum) // partial_sum(sum))
od
]|;
ParSummer7 = system |[
var
to_process : list[10] of t_int = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0];
in_progress : bool = false;
sum_index : t_index = 0;
sum : t_parsum = 0
methods
finished : bool =