Skip to content

Commit

Permalink
sample cleanup
Browse files Browse the repository at this point in the history 
fix to heuristic for variable elimination
  • Loading branch information
@shazqadeer
shazqadeer committed Jan 11, 2023
1 parent 76b6a37 commit 0e0366b
Show file tree
Hide file tree
Showing 4 changed files with 56 additions and 95 deletions.
9 changes: 8 additions & 1 deletion Source/Concurrency/TransitionRelationComputation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -348,7 +348,14 @@ private void SetDefinedVariables()
private void EliminateIntermediateVariables()
{
TryElimination(Enumerable.Empty<Variable>());
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)
Expand Down
7 changes: 3 additions & 4 deletions Test/civl/inductive-sequentialization/BroadcastConsensus.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
{
Expand Down
133 changes: 44 additions & 89 deletions Test/civl/inductive-sequentialization/NBuyer.bpl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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] }
Expand Down Expand Up @@ -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)
}

////////////////////////////////////////////////////////////////////////////////
Expand All @@ -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
Expand All @@ -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;
}

Expand All @@ -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));
}

Expand All @@ -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));
}
}
Expand All @@ -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);
}

////////////////////////////////////////////////////////////////////////////////
Expand All @@ -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));
}

Expand All @@ -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));
}
}
Expand All @@ -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);
}

////////////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -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;
}
Expand All @@ -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);
Expand All @@ -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;
}
Expand All @@ -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);
Expand All @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion Test/civl/inductive-sequentialization/NBuyer.bpl.expect
View file
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Boogie program verifier finished with 130 verified, 0 errors
Boogie program verifier finished with 132 verified, 0 errors

0 comments on commit 0e0366b

Please sign in to comment.