Skip to content

Commit

Permalink
further cleanup of refinement instrumentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer committed Jan 4, 2020
1 parent 7eddc91 commit 044e533
Showing 1 changed file with 33 additions and 57 deletions.
90 changes: 33 additions & 57 deletions Source/Concurrency/RefinementInstrumentation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,13 +75,11 @@ public override List<Cmd> CreateAssertCmds()

public override List<Cmd> CreateUnchangedGlobalsAssertCmds()
{
var cmds = new List<Cmd>();
var assertExpr = Expr.And(this.oldGlobalMap.Select(kvPair => Expr.Eq(Expr.Ident(kvPair.Key), Expr.Ident(kvPair.Value))));
assertExpr.Typecheck(new TypecheckingContext(null));
AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
skipAssertCmd.ErrorData = "Globals must not be modified";
cmds.Add(skipAssertCmd);
return cmds;
return new List<Cmd> { skipAssertCmd };
}
}

Expand All @@ -91,8 +89,8 @@ class ActionRefinementInstrumentation : SkipRefinementInstrumentation
private List<Variable> newLocalVars;
private Variable pc;
private Variable ok;
private Expr alpha;
private Expr beta;
private Expr gate;
private Expr transitionRelation;

private Dictionary<AtomicAction, Expr> transitionRelationCache;

Expand Down Expand Up @@ -153,86 +151,74 @@ public ActionRefinementInstrumentation(

Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);
Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
Expr betaExpr = GetTransitionRelation(atomicAction);
beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
Expr alphaExpr = Expr.And(atomicAction.gate.Select(g => g.Expr));
alphaExpr.Type = Type.Bool;
alpha = Substituter.Apply(always, alphaExpr);
Expr transitionRelationExpr = GetTransitionRelation(atomicAction);
transitionRelation = Substituter.ApplyReplacingOldExprs(always, forold, transitionRelationExpr);
Expr gateExpr = Expr.And(atomicAction.gate.Select(g => g.Expr));
gateExpr.Type = Type.Bool;
gate = Substituter.Apply(always, gateExpr);
}

public override List<Variable> NewLocalVars => newLocalVars;

public override List<Cmd> CreateInitCmds()
{
var cmds = new List<Cmd>();
List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));
rhss.Add(Expr.False);
lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));
rhss.Add(Expr.False);
cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
List<AssignLhs> lhss = new List<AssignLhs> {
new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)),
new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))
};
List<Expr> rhss = new List<Expr> { Expr.False, Expr.False };
var cmds = new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) };
cmds.AddRange(CreateUpdatesToOldOutputVars());
return cmds;
}

public override List<Cmd> CreateAssumeCmds()
{
var cmds = new List<Cmd>();
// assume pc || alpha(i, g);
Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
// assume pc || gate(i, g);
Expr assumeExpr = Expr.Or(Expr.Ident(pc), gate);
assumeExpr.Type = Type.Bool;
cmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
return cmds;
return new List<Cmd> { new AssumeCmd(Token.NoToken, assumeExpr) };
}

public override List<Cmd> CreateAssertCmds()
{
Expr assertExpr;
var cmds = new List<Cmd>();

// assert pc || g_old == g || beta(i, g_old, o, g);
assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(OldEqualityExprForGlobals(), beta));
// assert pc || g_old == g || transitionRelation(i, g_old, o, g);
assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(OldEqualityExprForGlobals(), transitionRelation));
assertExpr.Typecheck(new TypecheckingContext(null));
var skipOrBetaAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
skipOrBetaAssertCmd.ErrorData = "Transition invariant violated in initial state";
cmds.Add(skipOrBetaAssertCmd);
var skipOrTransitionRelationAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
skipOrTransitionRelationAssertCmd.ErrorData = "Transition invariant violated in initial state";

// assert pc ==> o_old == o && g_old == g;
assertExpr = Expr.Imp(Expr.Ident(pc), OldEqualityExpr());
// assert pc ==> g_old == g && o_old == o;
assertExpr = Expr.Imp(Expr.Ident(pc), Expr.And(OldEqualityExprForGlobals(), OldEqualityExprForOutputs()));
assertExpr.Typecheck(new TypecheckingContext(null));
AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
skipAssertCmd.ErrorData = "Transition invariant violated in final state";
cmds.Add(skipAssertCmd);
return cmds;
return new List<Cmd> { skipOrTransitionRelationAssertCmd, skipAssertCmd };
}

public override List<Cmd> CreateReturnAssertCmds()
{
var cmds = CreateUnchangedOutputsAssertCmds();
AssertCmd assertCmd = new AssertCmd(Token.NoToken, Expr.Ident(ok));
assertCmd.ErrorData = "Failed to execute atomic action before procedure return";
cmds.Add(assertCmd);
return cmds;
return new List<Cmd> { assertCmd };
}

public override List<Cmd> CreateUnchangedOutputsAssertCmds()
{
// assert pc ==> o_old == o;
var cmds = new List<Cmd>();
Expr bb = OldEqualityExprForOutputs();
var assertExpr = Expr.Imp(Expr.Ident(pc), bb);
var assertExpr = Expr.Imp(Expr.Ident(pc), OldEqualityExprForOutputs());
assertExpr.Typecheck(new TypecheckingContext(null));
AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
skipAssertCmd.ErrorData = "Outputs must not be modified";
cmds.Add(skipAssertCmd);
return cmds;
return new List<Cmd> { skipAssertCmd };
}

public override List<Cmd> CreateUpdatesToRefinementVars()
{
// pc, ok := g_old == g ==> pc, beta(i, g_old, o, g) || o_old == o && ok;
Expr aa = OldEqualityExprForGlobals();
// pc := g_old == g ==> pc;
// ok := transitionRelation(i, g_old, o, g) || (o_old == o && ok);
List<AssignLhs> pcUpdateLHS = new List<AssignLhs>
{
new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)),
Expand All @@ -241,14 +227,14 @@ public override List<Cmd> CreateUpdatesToRefinementVars()
List<Expr> pcUpdateRHS = new List<Expr>(
new Expr[]
{
Expr.Imp(aa, Expr.Ident(pc)),
Expr.Or(beta, Expr.And(OldEqualityExprForOutputs(), Expr.Ident(ok))),
Expr.Imp(OldEqualityExprForGlobals(), Expr.Ident(pc)),
Expr.Or(transitionRelation, Expr.And(OldEqualityExprForOutputs(), Expr.Ident(ok))),
});
foreach (Expr e in pcUpdateRHS)
{
e.Typecheck(new TypecheckingContext(null));
}
return new List<Cmd> {new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS)};
return new List<Cmd> { new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS) };
}

public override List<Cmd> CreateUpdatesToOldOutputVars()
Expand All @@ -260,12 +246,7 @@ public override List<Cmd> CreateUpdatesToOldOutputVars()
lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOutputMap[o])));
rhss.Add(Expr.Ident(o));
}
var cmds = new List<Cmd>();
if (lhss.Count > 0)
{
cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
}
return cmds;
return lhss.Count > 0 ? new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) } : new List<Cmd>();
}

private Expr GetTransitionRelation(AtomicAction atomicAction)
Expand All @@ -279,11 +260,6 @@ private Expr GetTransitionRelation(AtomicAction atomicAction)
return transitionRelationCache[atomicAction];
}

private Expr OldEqualityExpr()
{
return Expr.And(OldEqualityExprForGlobals(), OldEqualityExprForOutputs());
}

private Expr OldEqualityExprForGlobals()
{
return Expr.And(this.oldGlobalMap.Select(kvPair => Expr.Eq(Expr.Ident(kvPair.Key), Expr.Ident(kvPair.Value))));
Expand Down

0 comments on commit 044e533

Please sign in to comment.