diff --git a/Source/Concurrency/TransitionRelationComputation.cs b/Source/Concurrency/TransitionRelationComputation.cs index ac08ae393..da1a8e5af 100644 --- a/Source/Concurrency/TransitionRelationComputation.cs +++ b/Source/Concurrency/TransitionRelationComputation.cs @@ -348,7 +348,14 @@ private void SetDefinedVariables() private void EliminateIntermediateVariables() { TryElimination(Enumerable.Empty()); - TryElimination(trc.allLocVars.Select(v => varCopies[v][0])); + if (trc.allLocVars.Count > 0) + { + for (int i = 1; i <= trc.allLocVars.Select(v => varCopies[v].Count).Max(); i++) + { + TryElimination(trc.allLocVars.SelectMany(v => + varCopies[v].GetRange(0, i <= varCopies[v].Count ? i : varCopies[v].Count))); + } + } TryElimination(trc.allLocVars.Where(v => v.FindAttribute("pool") != null).SelectMany(v => varCopies[v])); if (trc.ignorePostState) diff --git a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl index bf404accb..4807d9476 100644 --- a/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl +++ b/Test/civl/inductive-sequentialization/BroadcastConsensus.bpl @@ -47,13 +47,12 @@ function max(CH:[val]int) : val; function card(CH:[val]int) : int; axiom card(MultisetEmpty) == 0; -axiom (forall v:val :: card(MultisetSingleton(v)) == 1); axiom (forall CH:[val]int, v:val :: card(MultisetPlus(CH, MultisetSingleton(v))) == card(CH) + 1); -axiom (forall CH:[val]int, v:val :: {CH[v := CH[v] + 1]} card(CH[v := CH[v] + 1]) == card(CH) + 1); -axiom (forall m:[val]int, m':[val]int :: {card(m), card(m')} MultisetSubsetEq(m, m') && card(m) == card(m') ==> m == m'); +axiom (forall CH:[val]int, v:val, x:int :: card(CH[v := x]) == card(CH) + x - CH[v]); +axiom (forall m:[val]int, m':[val]int :: MultisetSubsetEq(m, m') && card(m) == card(m') ==> m == m'); axiom (forall v:val :: max(MultisetSingleton(v)) == v); -axiom (forall CH:[val]int, v:val :: { CH[v := CH[v] + 1] } max(CH[v := CH[v] + 1]) == (if v > max(CH) then v else max(CH))); +axiom (forall CH:[val]int, v:val, x:int :: max(CH[v := x]) == (if v > max(CH) && x > 0 then v else max(CH))); function value_card(v:val, value:[pid]val, i:pid, j:pid) : int { diff --git a/Test/civl/inductive-sequentialization/NBuyer.bpl b/Test/civl/inductive-sequentialization/NBuyer.bpl index a1be54f04..a7b2dcf94 100644 --- a/Test/civl/inductive-sequentialization/NBuyer.bpl +++ b/Test/civl/inductive-sequentialization/NBuyer.bpl @@ -33,7 +33,7 @@ function {:constructor} SellerInit(pid:int) : PA; function {:constructor} SellerFinish(pid:int) : PA; function {:inline} NoPAs () : [PA]int -{ (lambda pa:PA :: 0) } +{ MapConst(0) } function {:inline} SingletonPA (pa:PA) : [PA]int { NoPAs()[pa := 1] } @@ -61,10 +61,10 @@ function {:inline} Init(pids:[int]bool, ReqCH:int, QuoteCH:[int][int]int, { pids == MapConst(true) && ReqCH == 0 && - QuoteCH == (lambda i:int :: (lambda q:int :: 0)) && - RemCH == (lambda i:int :: (lambda r:int :: 0)) && - DecCH == (lambda b:bool :: 0) && - contribution == (lambda i:int :: 0) + QuoteCH == (lambda i:int :: MapConst(0)) && + RemCH == (lambda i:int :: MapConst(0)) && + DecCH == MapConst(0) && + contribution == MapConst(0) } //////////////////////////////////////////////////////////////////////////////// @@ -86,7 +86,7 @@ modifies DecCH, contribution; havoc contribution; if (*) { - DecCH := (lambda b:bool :: if b == (sum(contribution, 1, n) == price) then 1 else 0); + DecCH := MapConst(0)[(sum(contribution, 1, n) == price) := 1]; PAs := SingletonPA(SellerFinish(0)); } else @@ -101,8 +101,8 @@ modifies DecCH; { var dec:bool; assert sellerID(pid); - assert DecCH == (lambda b:bool :: if b == (sum(contribution, 1, n) == price) then 1 else 0); dec := (sum(contribution, 1, n) == price); + assert DecCH == MapConst(0)[dec := 1]; DecCH[dec] := DecCH[dec] - 1; } @@ -116,7 +116,7 @@ modifies DecCH, contribution; { assert Init(pids, ReqCH, QuoteCH, RemCH, DecCH, contribution); havoc contribution; - DecCH := (lambda b:bool :: if b == (sum(contribution, 1, n) == price) then 1 else 0); + DecCH := MapConst(0)[(sum(contribution, 1, n) == price) := 1]; PAs := SingletonPA(SellerFinish(0)); } @@ -126,37 +126,38 @@ returns ({:pending_async "SellerFinish","FirstBuyer","MiddleBuyer","LastBuyer"} modifies QuoteCH, RemCH, DecCH, contribution; { var {:pool "INV3"} k: int; + var {:pool "contribution"} c: [int]int; assert Init(pids, ReqCH, QuoteCH, RemCH, DecCH, contribution); - havoc contribution; + contribution := c; assume {:add_to_pool "INV3", 0, 1, k, k+1, n} true; if (*) { - QuoteCH := (lambda i:int :: (lambda q:int :: if buyerID(i) && q == price then 1 else 0)); + QuoteCH := (lambda i:int :: if buyerID(i) then MapConst(0)[price := 1] else MapConst(0)); PAs := MapAddPA4(SellerFinish(0), FirstBuyer(1), LastBuyer(n), (lambda pa:PA :: if pa is MiddleBuyer && middleBuyerID(pa->pid) then 1 else 0)); choice := FirstBuyer(1); } else if (*) { assume 1 <= k && k < n && 0 <= sum(contribution, 1, k) && sum(contribution, 1, k) <= price; - QuoteCH := (lambda i:int :: (lambda q:int :: if buyerID(i) && i > k && q == price then 1 else 0)); - RemCH := (lambda i:int :: (lambda r:int :: if i == k+1 && r == price - sum(contribution, 1, k) then 1 else 0)); + QuoteCH := (lambda i:int :: if buyerID(i) && i > k then MapConst(0)[price := 1] else MapConst(0)); + RemCH := (lambda i:int :: if i == k+1 then MapConst(0)[(price - sum(contribution, 1, k)) := 1] else MapConst(0)); PAs := MapAddPA3(SellerFinish(0), LastBuyer(n), (lambda pa:PA :: if pa is MiddleBuyer && middleBuyerID(pa->pid) && pa->pid > k then 1 else 0)); choice := if lastBuyerID(k+1) then LastBuyer(k+1) else MiddleBuyer(k+1); } else if (*) { - QuoteCH := (lambda i:int :: (lambda q:int :: if lastBuyerID(i) && q == price then 1 else 0)); + QuoteCH := (lambda i:int :: if lastBuyerID(i) then MapConst(0)[price := 1] else MapConst(0)); assume 0 <= sum(contribution, 1, n-1) && sum(contribution, 1, n-1) <= price; - RemCH := (lambda i:int :: (lambda r:int :: if i == n && r == price - sum(contribution, 1, n-1) then 1 else 0)); + RemCH := (lambda i:int :: if i == n then MapConst(0)[(price - sum(contribution, 1, n-1)) := 1] else MapConst(0)); PAs := MapAddPA(SingletonPA(SellerFinish(0)), SingletonPA(LastBuyer(n))); choice := LastBuyer(n); } else { - DecCH := (lambda b:bool :: if b == (sum(contribution, 1, n) == price) then 1 else 0); + DecCH := MapConst(0)[(sum(contribution, 1, n) == price) := 1]; PAs := SingletonPA(SellerFinish(0)); } } @@ -165,85 +166,35 @@ procedure {:IS_abstraction}{:layer 4} FirstBuyer' ({:linear_in "pid"} pid:int) modifies QuoteCH, RemCH, contribution; { - var rem:int; - var amount:int; - - assert firstBuyerID(pid); - assert (forall q:int :: QuoteCH[pid][q] > 0 ==> q == price); - - assert DecCH == (lambda b:bool :: 0); - assert (forall i:int :: i != pid ==> RemCH[i] == (lambda r:int :: 0)); - + assert DecCH == MapConst(0); + assert (forall i:int :: i != pid ==> RemCH[i] == MapConst(0)); assert QuoteCH[pid][price] > 0; - QuoteCH[pid][price] := QuoteCH[pid][price] - 1; - - rem := price; - if (*) { amount := min(wallet, rem); } else { amount := 0; } - contribution[pid] := amount; - rem := rem - amount; - RemCH[nextBuyer(pid)][rem] := RemCH[nextBuyer(pid)][rem] + 1; + call FirstBuyer(pid); } procedure {:IS_abstraction}{:layer 4} MiddleBuyer' ({:linear_in "pid"} pid:int) modifies QuoteCH, RemCH, contribution; { - var rem:int; - var amount:int; - - assert middleBuyerID(pid); - assert (forall q:int :: QuoteCH[pid][q] > 0 ==> q == price); - assert (forall r:int :: RemCH[pid][r] > 0 ==> 0 <= r && r <= price); assert (forall r:int :: RemCH[pid][r] > 0 ==> r == price - sum(contribution, 1, pid - 1)); assert RemCH[pid][price - sum(contribution, 1, pid - 1)] > 0; - assert DecCH == (lambda b:bool :: 0); - assert (forall i:int :: i < pid ==> QuoteCH[i] == (lambda r:int :: 0)); - assert (forall i:int :: i != pid ==> RemCH[i] == (lambda r:int :: 0)); - + assert DecCH == MapConst(0); + assert (forall i:int :: i < pid ==> QuoteCH[i] == MapConst(0)); + assert (forall i:int :: i != pid ==> RemCH[i] == MapConst(0)); assert QuoteCH[pid][price] > 0; - assume RemCH[pid][rem] > 0; - - QuoteCH[pid][price] := QuoteCH[pid][price] - 1; - RemCH[pid][rem] := RemCH[pid][rem] - 1; - - if (*) { amount := min(wallet, rem); } else { amount := 0; } - contribution[pid] := amount; - rem := rem - amount; - RemCH[nextBuyer(pid)][rem] := RemCH[nextBuyer(pid)][rem] + 1; + call MiddleBuyer(pid); } procedure {:IS_abstraction}{:layer 4} LastBuyer' ({:linear_in "pid"} pid:int) modifies QuoteCH, RemCH, DecCH, contribution; { - var rem:int; - var amount:int; - - assert lastBuyerID(pid); - assert (forall q:int :: QuoteCH[pid][q] > 0 ==> q == price); - assert (forall r:int :: RemCH[pid][r] > 0 ==> 0 <= r && r <= price); assert (forall r:int :: RemCH[pid][r] > 0 ==> r == price - sum(contribution, 1, pid - 1)); assert RemCH[n][price - sum(contribution, 1, n-1)] > 0; - assert DecCH == (lambda b:bool :: 0); - assert (forall i:int :: i < pid ==> QuoteCH[i] == (lambda r:int :: 0)); - + assert DecCH == MapConst(0); + assert (forall i:int :: i < pid ==> QuoteCH[i] == MapConst(0)); assert QuoteCH[pid][price] > 0; - assume RemCH[pid][rem] > 0; - - QuoteCH[pid][price] := QuoteCH[pid][price] - 1; - RemCH[pid][rem] := RemCH[pid][rem] - 1; - - if (*) { amount := min(wallet, rem); } else { amount := 0; } - contribution[pid] := amount; - - if (amount == rem) - { - DecCH[true] := DecCH[true] + 1; - } - else - { - DecCH[false] := DecCH[false] + 1; - } + call LastBuyer(pid); } //////////////////////////////////////////////////////////////////////////////// @@ -255,7 +206,8 @@ returns ({:pending_async "SellerFinish","FirstBuyer","MiddleBuyer","LastBuyer"} modifies QuoteCH; { assert Init(pids, ReqCH, QuoteCH, RemCH, DecCH, contribution); - QuoteCH := (lambda i:int :: (lambda q:int :: if buyerID(i) && q == price then 1 else 0)); + assume {:add_to_pool "contribution", contribution} true; + QuoteCH := (lambda i:int :: if buyerID(i) then MapConst(0)[price := 1] else MapConst(0)); PAs := MapAddPA4(SellerFinish(0), FirstBuyer(1), LastBuyer(n), (lambda pa:PA :: if pa is MiddleBuyer && middleBuyerID(pa->pid) then 1 else 0)); } @@ -272,7 +224,7 @@ modifies ReqCH, QuoteCH; } else { - QuoteCH := (lambda i:int :: (lambda q:int :: if buyerID(i) && q == price then 1 else 0)); + QuoteCH := (lambda i:int :: if buyerID(i) then MapConst(0)[price := 1] else MapConst(0)); PAs := MapAddPA4(SellerFinish(0), FirstBuyer(1), LastBuyer(n), (lambda pa:PA :: if pa is MiddleBuyer && middleBuyerID(pa->pid) then 1 else 0)); } } @@ -282,14 +234,9 @@ SellerInit' ({:linear_in "pid"} pid:int) returns ({:pending_async "SellerFinish"} PAs:[PA]int) modifies ReqCH, QuoteCH; { - assert sellerID(pid); - assert QuoteCH == (lambda i:int :: (lambda q:int :: 0)); // To discharge gate failure preservation for FirstBuyer/MiddleBuyer/LastBuyer - + assert QuoteCH == (lambda i:int :: MapConst(0)); // To discharge gate failure preservation for FirstBuyer/MiddleBuyer/LastBuyer assert ReqCH > 0; - ReqCH := ReqCH - 1; - - QuoteCH := (lambda i:int :: (lambda q:int :: if buyerID(i) && q == price then QuoteCH[i][q] + 1 else QuoteCH[i][q])); - PAs := SingletonPA(SellerFinish(pid)); + call PAs := SellerInit(pid); } //////////////////////////////////////////////////////////////////////////////// @@ -385,6 +332,7 @@ modifies QuoteCH, RemCH, contribution; rem := price; if (*) { amount := min(wallet, rem); } else { amount := 0; } contribution[pid] := amount; + assume {:add_to_pool "contribution", contribution} true; rem := rem - amount; RemCH[nextBuyer(pid)][rem] := RemCH[nextBuyer(pid)][rem] + 1; } @@ -393,8 +341,8 @@ procedure {:atomic}{:layer 2,4} MiddleBuyer ({:linear_in "pid"} pid:int) modifies QuoteCH, RemCH, contribution; { - var rem:int; - var amount:int; + var {:pool "rem"} rem:int; + var {:pool "amount"} amount:int; assert middleBuyerID(pid); assert (forall q:int :: QuoteCH[pid][q] > 0 ==> q == price); @@ -408,6 +356,10 @@ modifies QuoteCH, RemCH, contribution; if (*) { amount := min(wallet, rem); } else { amount := 0; } contribution[pid] := amount; + assume + {:add_to_pool "contribution", contribution} + {:add_to_pool "rem", rem} + {:add_to_pool "amount", amount} true; rem := rem - amount; RemCH[nextBuyer(pid)][rem] := RemCH[nextBuyer(pid)][rem] + 1; } @@ -416,8 +368,8 @@ procedure {:atomic}{:layer 2,4} LastBuyer ({:linear_in "pid"} pid:int) modifies QuoteCH, RemCH, DecCH, contribution; { - var rem:int; - var amount:int; + var {:pool "rem"} rem:int; + var {:pool "amount"} amount:int; assert lastBuyerID(pid); assert (forall q:int :: QuoteCH[pid][q] > 0 ==> q == price); @@ -431,7 +383,10 @@ modifies QuoteCH, RemCH, DecCH, contribution; if (*) { amount := min(wallet, rem); } else { amount := 0; } contribution[pid] := amount; - + assume + {:add_to_pool "contribution", contribution} + {:add_to_pool "rem", rem} + {:add_to_pool "amount", amount} true; if (amount == rem) { DecCH[true] := DecCH[true] + 1; diff --git a/Test/civl/inductive-sequentialization/NBuyer.bpl.expect b/Test/civl/inductive-sequentialization/NBuyer.bpl.expect index 2e51eecea..afbf66a39 100644 --- a/Test/civl/inductive-sequentialization/NBuyer.bpl.expect +++ b/Test/civl/inductive-sequentialization/NBuyer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 130 verified, 0 errors +Boogie program verifier finished with 132 verified, 0 errors