Commit 40b1da4b authored by Alfons Laarman's avatar Alfons Laarman
Browse files

Physically replace var references in identifiers

parent d8964773
......@@ -19,7 +19,6 @@ import static spins.promela.compiler.parser.Promela.C_STATE_PROC_COUNTER;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
import spins.promela.compiler.automaton.Automaton;
import spins.promela.compiler.automaton.State;
......@@ -72,18 +71,6 @@ public class Proctype implements VariableContainer {
* The store where all the variables are stored.
*/
protected final VariableStore varStore;
public void addVariableMapping(String s, String v) {
varStore.addVariableMapping(s, v);
}
public String getVariableMapping(String s) {
return varStore.getVariableMapping(s);
}
public Map<String, String> getVariableMappings() {
return varStore.getVariableMappings();
}
/**
* The expression which can enable or disable all actions.
......
......@@ -35,9 +35,9 @@ public class Identifier extends Expression {
@SuppressWarnings("unused")
private static final long serialVersionUID = -5928789117017713005L;
private final Variable var;
private Variable var;
private final Expression arrayExpr;
private Expression arrayExpr;
private int instanceIndex = -1; // no instance index
......@@ -237,4 +237,12 @@ public class Identifier extends Expression {
return false;
}
}
public void setVariable(Variable v) {
this.var = v;
}
public void setArrayIndex(Expression e) {
arrayExpr = e;
}
}
......@@ -128,6 +128,31 @@ public class LTSminTreeWalker {
public List<ReadAction> reads = new ArrayList<ReadAction>();
public List<SendAction> writes = new ArrayList<SendAction>();
private List<Identifier> ids = new ArrayList<Identifier>();
private Identifier newid(Variable elemVar) {
Identifier identifier = new Identifier(elemVar);
ids.add(identifier);
return identifier;
}
private Expression newid(Token token, Variable newVar, Expression arrayExpr, Identifier sub) {
Identifier newId = new Identifier(token, newVar, arrayExpr, sub);
ids.add(newId);
return newId;
}
private void replaceVars(Variable v, Identifier id) {
for (Identifier i : ids) {
if (i.getVariable() == v) {
i.setVariable(id.getVariable());
if (i.getArrayExpr() != null)
throw new AssertionError("Not a lhs var place holder: "+ i +" = "+ id);
i.setArrayIndex(id.getArrayExpr());
}
}
}
private final Specification spec;
static boolean NEVER;
static boolean LTSMIN_LTL = false;
......@@ -194,7 +219,7 @@ public class LTSminTreeWalker {
private void createModelAssertions(LTSminModel model) {
for (RemoteRef ref : spec.remoteRefs) {
ProcInstance instance = ref.getInstance();
Expression pid = id(instance.getPID());
Expression pid = newid(instance.getPID());
Expression left = eq(pid, constant(-1));
Expression right = eq(pid, constant(instance.getID()));
Expression condition = or(left, right);
......@@ -274,7 +299,7 @@ public class LTSminTreeWalker {
Expression or = null;
if (never.getStartState().isAcceptState()) {
Variable pc = never.getPC();
Expression g = compare(PromelaConstants.EQ, id(pc), constant(-1));
Expression g = compare(PromelaConstants.EQ, newid(pc), constant(-1));
or = or == null ? g : or(or, g) ; // Or
}
for (State s : never.getAutomaton()) {
......@@ -297,9 +322,9 @@ public class LTSminTreeWalker {
if (s.isProgressState()) {
Variable pc = pi.getPC();
Expression counter = constant(s.getStateId());
Expression e = compare(PromelaConstants.EQ, id(pc), counter);
Expression e = compare(PromelaConstants.EQ, newid(pc), counter);
or = or == null ? e : or(or, e);
Expression ne = compare(PromelaConstants.NEQ, id(pc), counter);
Expression ne = compare(PromelaConstants.NEQ, newid(pc), counter);
and = and == null ? ne : and(and, ne) ;
}
}
......@@ -315,11 +340,11 @@ public class LTSminTreeWalker {
}
/* Export label for valid end states */
Expression end = compare(PromelaConstants.EQ, id(_NR_PR), constant(0)); // or
Expression end = compare(PromelaConstants.EQ, newid(_NR_PR), constant(0)); // or
Expression and = null;
for (ProcInstance instance : spec) {
Variable pc = instance.getPC();
Expression labeled = compare(PromelaConstants.EQ, id(pc), constant(-1));
Expression labeled = compare(PromelaConstants.EQ, newid(pc), constant(-1));
for (State s : instance.getAutomaton()) {
if (s.hasLabelPrefix("end")) {
labeled = or(labeled, pcGuard(s, instance).getExpr()); // Or
......@@ -349,7 +374,7 @@ public class LTSminTreeWalker {
Variable pc = pi.getPC();
Expression counter = constant(s.getStateId());
Expression e = compare(PromelaConstants.EQ, id(pc), counter);
Expression e = compare(PromelaConstants.EQ, newid(pc), counter);
e = x == null ? e : or(e, x);
model.addStateLabel(label, new LTSminGuard(e));
//System.out.println("Adding label "+ label +" --> "+ e);
......@@ -465,10 +490,6 @@ public class LTSminTreeWalker {
instance.addVariable(newvar, p.getArguments().contains(var));
}
instance.lastArgument();
for (String mapped : p.getVariableMappings().keySet()) {
String to = p.getVariableMapping(mapped);
instance.addVariableMapping(mapped, to);
}
HashMap<State, State> seen = new HashMap<State, State>();
instantiate(p.getStartState(), instance.getStartState(), seen, instance);
new RenumberAll().optimize(instance.getAutomaton());
......@@ -637,7 +658,7 @@ public class LTSminTreeWalker {
if (write) newVar.setAssignedTo();
Expression arrayExpr = instantiate(id.getArrayExpr(), p, write);
Identifier sub = (Identifier)instantiate(id.getSub(), p, write);
return new Identifier(id.getToken(), newVar, arrayExpr, sub);
return newid(id.getToken(), newVar, arrayExpr, sub);
} else if (e instanceof AritmicExpression) {
AritmicExpression ae = (AritmicExpression)e;
Expression ex1 = instantiate(ae.getExpr1(), p, write);
......@@ -750,6 +771,21 @@ public class LTSminTreeWalker {
}
}
List<Variable> remove = new LinkedList<Variable>();
for (Variable v : spec.getVariableStore().getVariables()) {
Expression init = v.getInitExpr();
if (!(v instanceof ChannelVariable) || null == init) continue;
if (!(init instanceof Identifier)) throw new AssertionError("No ID:"+ init +" Init of: "+ v);
Identifier id = (Identifier) init;
System.out.println(v.getName() +" --> "+ id.toString());
replaceVars (v, id);
remove.add(v);
}
for (Variable v : remove) {
spec.getVariableStore().delVariable(v);
}
// Update the spec with the results
spec.clearReadActions();
spec.clearWriteActions();
......@@ -786,19 +822,18 @@ public class LTSminTreeWalker {
throw new AssertionError("Cannot dynamically bind "+ target.getTypeName() +" to the run expressions in presence of arguments of type channel.\n" +
"Change the proctype's arguments or unroll the loop with run expressions in the model.");
String name = v.getName();
debug.say(MessageKind.DEBUG, "Binding "+ target +"."+ name +" to "+ varParameter.getOwner() +"."+ varParameter.getName());
v.setDisplayName(v.getName());
v.setType(varParameter.getType());
v.setOwner(varParameter.getOwner());
v.setName(varParameter.getName());
debug.say(MessageKind.DEBUG, "Binding "+ target +"."+ name +" to "+ varParameter.toString());
if (varParameter.getArraySize() > -1) {
try {
int c = id.getArrayExpr().getConstantValue();
v.setArrayIndex(c);
id.getArrayExpr().getConstantValue();
} catch (ParseException e) {
throw new AssertionError("Cannot () statically bind "+ target.getTypeName() +" to the run expressions without constant channel array index.");
}
}
replaceVars (v, id);
} else if (!dynamic) {
try {
v.setInitExpr(param);
......@@ -820,7 +855,7 @@ public class LTSminTreeWalker {
Expression init = v.getInitExpr();
v.unsetInitExpr();
v.setAssignedTo();
re.addInitAction(new AssignAction(new Token(PromelaConstants.ASSIGN), id(v), init));
re.addInitAction(new AssignAction(new Token(PromelaConstants.ASSIGN), newid(v), init));
}
}
}
......@@ -1098,7 +1133,7 @@ public class LTSminTreeWalker {
AssignAction aa = (AssignAction)action;
if (aa.getExpr() instanceof RunExpression) {
lt.addAction(new ExprAction(aa.getExpr()));
aa.setExpr(calc(PromelaConstants.MINUS, id(_NR_PR), constant(1)));
aa.setExpr(calc(PromelaConstants.MINUS, newid(_NR_PR), constant(1)));
}
}
lt.addAction(action);
......
......@@ -176,7 +176,7 @@ public class LTSminStateVector extends LTSminSubVectorStruct
* Add a variable declaration to struct
*/
private void addVariable(LTSminTypeStruct struct, Variable var, LTSminDebug debug) {
if (var.isHidden() || !var.getName().equals(var.getDisplayName())) return;
if (var.isHidden()) return;
String name = var.getName();
LTSminVariable lvar = null;
......
......@@ -88,10 +88,6 @@ public class LTSminUtil {
return new Identifier(new Token(IDENTIFIER,v.getName()), v, null);
}
public static Identifier id(Variable v, int c) {
return new Identifier(new Token(IDENTIFIER,v.getName()), v, constant(c), null);
}
public static Identifier id(Variable v, Expression arrayExpr, Identifier sub) {
return new Identifier(new Token(IDENTIFIER,v.getName()), v, arrayExpr, sub);
}
......
......@@ -587,8 +587,8 @@ public class Promela implements PromelaConstants {
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
case IDENTIFIER:
id = jj_consume_token(IDENTIFIER);
store.addVariableMapping(var.getName(), id.image);
Variable var2 = store.getVariable(id.image);
var.setInitExpr(new Identifier(store.getVariable(id.image)));
store.addVariable(var);
break;
case LBRACK:
jj_consume_token(LBRACK);
......
......@@ -1049,8 +1049,8 @@ void ch_init(Token as, VariableContainer store, ChannelVariable var): {
}{
id=<IDENTIFIER>
{
store.addVariableMapping(var.getName(), id.image);
Variable var2 = store.getVariable(id.image); }
var.setInitExpr(new Identifier(store.getVariable(id.image)));
store.addVariable(var); }
|
<LBRACK> size=constant() <RBRACK> <OF>
{
......
......@@ -37,8 +37,6 @@ public class Variable {
private VariableType type;
private String displayName = null;
private boolean assignedTo = false;
private boolean hidden = false;
......@@ -61,7 +59,6 @@ public class Variable {
this.assignedTo = var.assignedTo;
this.arrayIndex = var.arrayIndex;
this.hidden = var.hidden;
this.displayName = var.displayName;
this.initExpr = var.initExpr;
}
......@@ -138,15 +135,7 @@ public class Variable {
*/
@Override
public String toString() {
return owner == null ? getDisplayName() : owner.getName() +"."+ getDisplayName();
}
public void setDisplayName(String name2) {
this.displayName = name2;
}
public String getDisplayName() {
return (null == displayName ? name : displayName);
return owner == null ? getName() : owner.getName() +"."+ getName();
}
public Variable setAssignedTo() {
......
......@@ -48,8 +48,4 @@ public interface VariableContainer {
* @return true when a variable with that name already exists or otherwise false.
*/
public boolean hasVariable(String name);
public void addVariableMapping(String s, String v);
public String getVariableMapping(String s);
}
......@@ -31,27 +31,12 @@ public class VariableStore implements VariableContainer {
private final Map<String, Variable> varNames;
private final List<Variable> vars;
private final Map<String, String> mapping;
public void addVariableMapping(String s, String v) {
mapping.put(s, v);
}
public String getVariableMapping(String s) {
return mapping.get(s);
}
public Map<String, String> getVariableMappings() {
return mapping;
}
/**
* Creates a new VariableStore.
*/
public VariableStore() {
vars = new LinkedList<Variable>();
varNames = new HashMap<String, Variable>();
mapping = new HashMap<String, String>();
}
/**
......@@ -87,12 +72,7 @@ public class VariableStore implements VariableContainer {
*/
public Variable getVariable(final String name) {
Variable var = varNames.get(name);
if (var != null)
return var;
String to = getVariableMapping(name);
if (null == to)
return null;
return getVariable(to);
return var;
}
/**
......@@ -111,11 +91,10 @@ public class VariableStore implements VariableContainer {
*/
public boolean hasVariable(final String name) {
Variable var = varNames.get(name);
if (var != null)
return true;
String to = getVariableMapping(name);
if (null == to)
return false;
return hasVariable(to);
return var != null;
}
public void delVariable(Variable v) {
vars.remove(v);
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment