diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-09-13 11:37:48 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-09-13 11:37:48 +0530 |
| commit | a65934dec9e0d859bc58b33acf663d45e9dfbc96 (patch) | |
| tree | 2b2e9933d2bdbf7b7c472dd20f0c04319750615e | |
| parent | df8b2acec2c1ceb866903e6783b10c6fd5d72289 (diff) | |
Added some extra functionality to Model code for corral
| -rw-r--r-- | Source/Model/Model.cs | 43 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 3 |
2 files changed, 43 insertions, 3 deletions
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs index 06f680fa..f54ebbef 100644 --- a/Source/Model/Model.cs +++ b/Source/Model/Model.cs @@ -443,7 +443,8 @@ namespace Microsoft.Boogie List<string> vars = new List<string>();
Dictionary<string, Element> valuations = new Dictionary<string, Element>();
readonly CapturedState previous;
- public readonly string Name;
+ // AL: Dropping "readonly" for corral
+ public /* readonly */ string Name { get; private set; }
public IEnumerable<string> Variables { get { return vars; } }
public IEnumerable<string> AllVariables {
@@ -477,6 +478,35 @@ namespace Microsoft.Boogie valuations.Add(varname, value);
}
+ // Change name of the state
+ public void ChangeName(string newName)
+ {
+ Name = newName;
+ }
+
+ // Change names of variables in this state
+ // (Used by corral)
+ internal void ChangeVariableNames(Dictionary<string, string> varNameMap)
+ {
+ var oldVars = vars;
+ var oldValuations = valuations;
+
+ vars = new List<string>();
+ valuations = new Dictionary<string, Element>();
+
+ foreach (var v in oldVars)
+ {
+ if (varNameMap.ContainsKey(v)) vars.Add(varNameMap[v]);
+ else vars.Add(v);
+ }
+
+ foreach (var kvp in oldValuations)
+ {
+ if (varNameMap.ContainsKey(kvp.Key)) valuations.Add(varNameMap[kvp.Key], kvp.Value);
+ else valuations.Add(kvp.Key, kvp.Value);
+ }
+ }
+
internal CapturedState(string name, CapturedState prev)
{
Name = name;
@@ -491,6 +521,17 @@ namespace Microsoft.Boogie states.Add(s);
return s;
}
+
+ // Change names of variables in all captured states
+ // (Used by corral)
+ public void ChangeVariableNames(Dictionary<string, string> varNameMap)
+ {
+ foreach (var s in states)
+ {
+ s.ChangeVariableNames(varNameMap);
+ }
+ }
+
#endregion
public Model()
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index cc1aa6c9..243eb8e0 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2917,8 +2917,6 @@ namespace VC var filename = CommandLineOptions.Clo.ModelViewFile;
if (model == null || filename == null) return;
- GetModelWithStates(model);
-
if (filename == "-") {
model.Write(Console.Out);
Console.Out.Flush();
@@ -3013,6 +3011,7 @@ namespace VC var cex = GenerateTraceMain(labels, model, mvInfo);
Debug.Assert(candidatesToExpand.Count == 0);
if (cex != null) {
+ GetModelWithStates(model);
callback.OnCounterexample(cex, null);
this.PrintModel(model);
}
|