|
class GroupPhase
values
secondRoundWinners = [<A>,<B>,<C>,<D>,<E>,<F>,<G>,<H>];
secondRoundRunnersUp = [<B>,<A>,<D>,<C>,<F>,<E>,<H>,<G>]
types
public Team = <Brazil> | <Norway> | <Morocco> | <Scotland> |
<Italy> | <Chile> | <Austria> | <Cameroon> |
<France> | <Denmark> | <SouthAfrica> | <SaudiArabia> |
<Nigeria> | <Paraguay> | <Spain> | <Bulgaria> |
<Holland> | <Mexico> | <Belgium> | <SouthKorea> |
<Germany> | <Yugoslavia> | <Iran> | <UnitedStates> |
<Rumania> | <England> | <Colombia> | <Tunisia> |
<Argentina> | <Croatia> | <Jamaica> | <Japan>;
public GroupName = <A> | <B> | <C> | <D> | <E> | <F> | <G> | <H>;
Score :: team : Team
won : nat
drawn : nat
lost : nat
points : nat
inv sc == sc.points = 3 * sc.won + sc.drawn;
instance variables
gps : map GroupName to set of Score :=
{ <A> |-> sc_init ({<Brazil>, <Norway>, <Morocco>, <Scotland>}),
<B> |-> sc_init ({<Italy>, <Chile>, <Austria>, <Cameroon>}),
<C> |-> sc_init ({<France>, <Denmark>, <SouthAfrica>,<SaudiArabia>}),
<D> |-> sc_init ({ <Nigeria>, <Paraguay>, <Spain>, <Bulgaria>}),
<E> |-> sc_init ({ <Holland>, <Mexico>, <Belgium>, <SouthKorea>}),
<F> |-> sc_init ({<Germany>, <Yugoslavia>, <Iran>, <UnitedStates>}),
<G> |-> sc_init ({<Rumania>, <England>, <Colombia>, <Tunisia>}),
<H> |-> sc_init ({<Argentina>, <Croatia>, <Jamaica>, <Japan>})};
inv forall gp in set rng gps &
(card gp = 4 and
forall sc in set gp & sc.won + sc.lost + sc.drawn <= 3)
functions
sc_init : set of Team -> set of Score
sc_init (ts) ==
{ mk_Score (t,0,0,0,0) | t in set ts };
clear_winner : set of Score -> bool
clear_winner (scs) ==
exists sc in set scs &
forall sc' in set scs \ {sc} & sc.points > sc'.points;
winner_by_more_wins : set of Score -> bool
winner_by_more_wins (scs) ==
exists sc in set scs &
forall sc' in set scs \ {sc} &
(sc.points > sc'.points) or
(sc.points = sc'.points and sc.won > sc'.won)
operations
public Win : Team * Team ==> ()
Win (wt,lt) ==
let gp in set dom gps be st {wt,lt} subset {sc.team | sc in set gps(gp)}
in gps := gps ++ { gp |->
{ if sc.team = wt
then mu(sc, won |-> sc.won + 1,
points |-> sc.points + 3)
else if sc.team = lt
then mu(sc, lost |-> sc.lost + 1)
else sc
| sc in set gps(gp)}}
pre exists gp in set dom gps & {wt,lt} subset {sc.team | sc in set gps(gp)};
Win2 (wt,lt: Team)
ext wr gps : map GroupName to set of Score
pre exists gp in set dom gps &
{wt,lt} subset {sc.team | sc in set gps(gp)}
post exists gp in set dom gps &
{wt,lt} subset {sc.team | sc in set gps(gp)}
and gps = gps~ ++
{ gp |->
{if sc.team = wt
then mu(sc, won |-> sc.won + 1,
points |-> sc.points + 3)
else if sc.team = lt
then mu(sc, lost |-> sc.lost + 1)
else sc
| sc in set gps(gp)}};
GroupWinner (gp:GroupName) t:Team
ext rd gps : map GroupName to set of Score
pre gp in set dom gps
post t in set {sc.team | sc in set gps(gp)} and
let sct = iota sc in set gps(gp) & sc.team = t
in
forall sc in set gps(gp) &
sc.team <> t => sct.points > sc.points or
sct.points = sc.points and sct.won > sc.won;
GroupRunnerUp (gp:GroupName) t:Team
ext rd gps : map GroupName to set of Score
pre gp in set dom gps
post let sc' in set gps(gp) be st
true --post_GroupWinner(gp,sc'.team,gps,gps)
in t in set {sc.team | sc in set gps(gp) \ {sc'}} and
let sct = iota sc in set gps(gp) \ {sc'} & sc.team = t
in forall sc in set gps(gp) \ {sc'} &
sc.team <> t => sct.points > sc.points or
sct.points = sc.points and sct.won > sc.won;
-- let stmt - lots of examples presumably
GroupWinner_expl : GroupName ==> Team
GroupWinner_expl (gp) ==
let sc in set gps(gp) be st
forall sc' in set gps(gp) \ {sc} &
(sc.points > sc'.points) or
(sc.points = sc'.points and sc.won > sc'.won)
in return sc.team
pre gp in set dom gps;
GroupRunnerUp_expl : GroupName ==> Team
GroupRunnerUp_expl (gp) ==
def t = GroupWinner(gp)
in let sct = iota sc in set gps(gp) & sc.team = t
in
let sc in set gps(gp) \ {sct} be st
forall sc' in set gps(gp) \ {sc,sct} &
(sc.points > sc'.points) or
(sc.points = sc'.points and sc.won > sc'.won)
in return sc.team
pre gp in set dom gps;
-- def stmt
SecondRound_expl : () ==> seq of (Team * Team)
SecondRound_expl () ==
def winners = { gp |-> GroupWinner_expl(gp) | gp in set dom gps };
runners_up = { gp |-> GroupRunnerUp_expl(gp) | gp in set dom gps}
in return ([mk_(winners(secondRoundWinners(i)),
runners_up(secondRoundRunnersUp(i))) | i in set {1,...,8}]);
-- assignment to state designator
-- c.f. earlier version of Win
Win_sd : Team * Team ==> ()
Win_sd (wt,lt) ==
let gp in set dom gps be st {wt,lt} subset {sc.team | sc in set gps(gp)}
in gps(gp) := { if sc.team = wt
then mu(sc, won |-> sc.won + 1,
points |-> sc.points + 3)
else if sc.team = lt
then mu(sc, lost |-> sc.lost + 1)
else sc
| sc in set gps(gp)}
pre exists gp in set dom gps & {wt,lt} subset {sc.team | sc in set gps(gp)};
-- conditional statements
GroupWinner_if : GroupName ==> Team
GroupWinner_if (gp) ==
if clear_winner(gps(gp))
then return ((iota sc in set gps(gp) &
forall sc' in set gps(gp) \ {sc} &
sc.points > sc'.points).team)
else if winner_by_more_wins(gps(gp))
then return ((iota sc in set gps(gp) &
forall sc' in set gps(gp) \ {sc} &
(sc.points > sc'.points) or
(sc.points = sc'.points and sc.won > sc'.won)).team)
else RandomElement ( {sc.team | sc in set gps(gp) &
forall sc' in set gps(gp) &
sc'.points <= sc.points} )
pre gp in set dom gps;
RandomElement : set of Team ==> Team
RandomElement (ts) ==
(dcl t:Team := let t' in set ts in t';
return (t));
public GroupWinner_cases : GroupName ==> Team
GroupWinner_cases (gp) ==
cases true:
(clear_winner(gps(gp))) ->
return ((iota sc in set gps(gp) &
forall sc' in set gps(gp) \ {sc} &
sc.points > sc'.points).team),
(winner_by_more_wins(gps(gp))) ->
return ((iota sc in set gps(gp) &
forall sc' in set gps(gp) \ {sc} &
(sc.points > sc'.points) or
(sc.points = sc'.points and sc.won > sc'.won)).team),
others -> RandomElement ( {sc.team | sc in set gps(gp) &
forall sc' in set gps(gp) &
sc'.points <= sc.points} )
end
pre gp in set dom gps;
-- for loops
GroupWinners: () ==> set of Team
GroupWinners () ==
(dcl winners : set of Team := {};
for all gp in set dom gps do
(dcl winner: Team := GroupWinner(gp);
winners := winners union {winner}
);
return winners
);
end GroupPhase
class UseGP
instance variables
gp : GroupPhase := new GroupPhase()
traces
InitBeforePlay :
let t1 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>}
in
let t2 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>} \ {t1}
in
let t3 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>} \ {t1,t2}
in
let t4 in set {<Brazil>, <Norway>, <Morocco>, <Scotland>} \ {t1,t2,t3}
in
(gp.Win(t1,t2);gp.Win(t1,t3);gp.Win(t1,t4);gp.Win(t2,t3);
gp.Win(t2,t4);gp.Win(t3,t4);gp.GroupWinner_cases(<A>)
)
end UseGP
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
