diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html index 94f270a..8106f23 100644 --- a/courseA/IM_Alloy.html +++ b/courseA/IM_Alloy.html @@ -191,30 +191,30 @@ } } -<c1>pred</c1> shippingOrReceiving[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>] { - plus[its.itemDB[itemId].count, quantity] < <c2>0</c2> <c1>implies</c1> { +<c1>pred</c1> receivingOrShipping[its, its': Inventory, itemId: ItemId, quantity: <c1>Int</c1>] { + <div style="background-color:#EDF7FF;"> plus[its.itemDB[itemId].count, quantity] < <c2>0</c2> <c1>implies</c1> { <c1>all</c1> itemId': ItemId | its'.itemDB[itemId'] = its.itemDB[itemId'] } - <c1>else</c1> { + <c1>else</c1> {</div> <c1>some</c1> it': Item | { <c1>no</c1> itemId2: ItemId | its.itemDB[itemId2] = it' its'.itemDB = its.itemDB ++ itemId -> it' it'.name = its.itemDB[itemId].name it'.count = plus[its.itemDB[itemId].count, quantity] } - } + <div style="background-color:#EDF7FF;"> } </div> } <c1>pred</c1> execute[] { - <c1>some disj</c1> its, its', its'', its''': Inventory, itemId: ItemId, n: Name | { + <div style="background-color:#EDF7FF;"> <c1>some disj</c1> its, its', its'', its''': Inventory, itemId: ItemId, n: Name | {</div> init[its] itemRegistration[its, its', itemId, <c2>100</c2>, n] - shippingOrReceiving[its', its'', itemId, -<c2>50</c2>] - shippingOrReceiving[its'', its''', itemId, -<c2>75</c2>] + <div style="background-color:#EDF7FF;"> receivingOrShipping[its', its'', itemId, -<c2>50</c2>] + receivingOrShipping[its'', its''', itemId, -<c2>75</c2>]</div> } } -<c1>run</c1> execute <c1>for</c1> <c2>2</c2> <c1>but</c1> <c2>4</c2> Inventory, <c2>8</c2> <c1>Int</c1> + <div style="background-color:#EDF7FF;"><c1>run</c1> execute <c1>for</c1> <c2>2</c2> <c1>but</c1> <c2>4</c2> Inventory, <c2>8</c2> <c1>Int</c1></div> </pre> </div>