Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions prism/src/parser/PrismParser.java
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ static class ExpressionPair { public Expression expr1 = null; public Expression
int typeCount = 0;
Token typeDupe = null;
Declaration global;
Module m = null;
parser.ast.Module m = null;
RenamedModule rm = null;
RewardStruct rs = null;
Expression init = null;
Expand Down Expand Up @@ -1027,15 +1027,15 @@ static class ExpressionPair { public Expression expr1 = null; public Expression

// Module
static final public
Module Module() throws ParseException {ExpressionIdent name = null;
parser.ast.Module Module() throws ParseException {ExpressionIdent name = null;
Declaration var = null;
Expression invar;
Command comm = null;
Module module = null;
parser.ast.Module module = null;
Token begin = null;
begin = jj_consume_token(MODULE);
name = IdentifierExpression();
module = new Module(name.getName());
module = new parser.ast.Module(name.getName());
label_6:
while (true) {
switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
Expand Down
8 changes: 4 additions & 4 deletions prism/src/parser/PrismParser.jj
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ ModulesFile ModulesFile() throws PrismLangException :
int typeCount = 0;
Token typeDupe = null;
Declaration global;
Module m = null;
parser.ast.Module m = null;
RenamedModule rm = null;
RewardStruct rs = null;
Expression init = null;
Expand Down Expand Up @@ -791,17 +791,17 @@ DeclarationType DeclarationVarType() :

// Module

Module Module() :
parser.ast.Module Module() :
{
ExpressionIdent name = null;
Declaration var = null;
Expression invar;
Command comm = null;
Module module = null;
parser.ast.Module module = null;
Token begin = null;
}
{
begin = <MODULE> name = IdentifierExpression() { module = new Module(name.getName()); }
begin = <MODULE> name = IdentifierExpression() { module = new parser.ast.Module(name.getName()); }
( var = Declaration() { module.addDeclaration(var); } )*
( <INVARIANT> invar = Expression(false, false) <ENDINVARIANT> { module.setInvariant(invar); } )?
( comm = Command() { module.addCommand(comm); } )*
Expand Down
2 changes: 1 addition & 1 deletion prism/src/parser/VarList.java
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ public VarList(ModulesFile modulesFile) throws PrismLangException
this();

int i, j, n, n2;
Module module;
parser.ast.Module module;
Declaration decl;

// First add all globals to the list
Expand Down
6 changes: 3 additions & 3 deletions prism/src/parser/visitor/ASTTraverse.java
Original file line number Diff line number Diff line change
Expand Up @@ -196,8 +196,8 @@ public Object visit(DeclarationIntUnbounded e) throws PrismLangException
}
public void visitPost(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(Module e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(Module e) throws PrismLangException
public void visitPre(parser.ast.Module e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(parser.ast.Module e) throws PrismLangException
{
// Note: a few classes override this method (e.g. SemanticCheck)
// so take care to update those versions if changing this method
Expand All @@ -216,7 +216,7 @@ public Object visit(Module e) throws PrismLangException
visitPost(e);
return null;
}
public void visitPost(Module e) throws PrismLangException { defaultVisitPost(e); }
public void visitPost(parser.ast.Module e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(Command e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(Command e) throws PrismLangException
Expand Down
8 changes: 4 additions & 4 deletions prism/src/parser/visitor/ASTTraverseModify.java
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ public Object visit(ModulesFile e) throws PrismLangException
}
n = e.getNumModules();
for (i = 0; i < n; i++) {
if (e.getModule(i) != null) e.setModule(i, (Module)(e.getModule(i).accept(this)));
if (e.getModule(i) != null) e.setModule(i, (parser.ast.Module)(e.getModule(i).accept(this)));
}
n = e.getNumSystemDefns();
for (i = 0; i < n; i++) {
Expand Down Expand Up @@ -211,8 +211,8 @@ public Object visit(DeclarationIntUnbounded e) throws PrismLangException
}
public void visitPost(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(Module e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(Module e) throws PrismLangException
public void visitPre(parser.ast.Module e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(parser.ast.Module e) throws PrismLangException
{
visitPre(e);
int i, n;
Expand All @@ -229,7 +229,7 @@ public Object visit(Module e) throws PrismLangException
visitPost(e);
return e;
}
public void visitPost(Module e) throws PrismLangException { defaultVisitPost(e); }
public void visitPost(parser.ast.Module e) throws PrismLangException { defaultVisitPost(e); }
// -----------------------------------------------------------------------------------
public void visitPre(Command e) throws PrismLangException { defaultVisitPre(e); }
public Object visit(Command e) throws PrismLangException
Expand Down
2 changes: 1 addition & 1 deletion prism/src/parser/visitor/ASTVisitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ public interface ASTVisitor
public Object visit(DeclarationArray e) throws PrismLangException;
public Object visit(DeclarationClock e) throws PrismLangException;
public Object visit(DeclarationIntUnbounded e) throws PrismLangException;
public Object visit(Module e) throws PrismLangException;
public Object visit(parser.ast.Module e) throws PrismLangException;
public Object visit(Command e) throws PrismLangException;
public Object visit(Updates e) throws PrismLangException;
public Object visit(Update e) throws PrismLangException;
Expand Down
10 changes: 5 additions & 5 deletions prism/src/parser/visitor/ModulesFileSemanticCheck.java
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ public ModulesFileSemanticCheck(ModulesFile modulesFile)
public void visitPost(ModulesFile e) throws PrismLangException
{
int i, j, n, n2;
Module m;
parser.ast.Module m;
Vector<String> v;

// Check for use of init...endinit _and_ var initial values
Expand Down Expand Up @@ -174,13 +174,13 @@ public void visitPost(DeclarationClock e) throws PrismLangException
}
}

public void visitPre(Module e) throws PrismLangException
public void visitPre(parser.ast.Module e) throws PrismLangException
{
// Register the fact we are entering a module
//inModule = e;
}

public Object visit(Module e) throws PrismLangException
public Object visit(parser.ast.Module e) throws PrismLangException
{
// Override this so we can keep track of when we are in an invariant
visitPre(e);
Expand All @@ -201,7 +201,7 @@ public Object visit(Module e) throws PrismLangException
return null;
}

public void visitPost(Module e) throws PrismLangException
public void visitPost(parser.ast.Module e) throws PrismLangException
{
// Register the fact we are leaving a module
//inModule = null;
Expand Down Expand Up @@ -230,7 +230,7 @@ public void visitPost(Update e) throws PrismLangException
int i, n;
String s, var;
Command c;
Module m;
parser.ast.Module m;
boolean isLocal, isGlobal;

// Register the fact we are leaving an update
Expand Down
2 changes: 1 addition & 1 deletion prism/src/parser/visitor/Rename.java
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ public void visitPost(Declaration e) throws PrismLangException
}
}

public void visitPost(Module e) throws PrismLangException
public void visitPost(parser.ast.Module e) throws PrismLangException
{
// New name for module is specied in RenamedModule
e.setName(rm.getName());
Expand Down
2 changes: 1 addition & 1 deletion prism/src/prism/ExplicitModel2MTBDD.java
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ public Model buildModel(explicit.Model modelExpl, List<State> statesList, Module
this.modulesFile = modulesFile;
} else {
this.modulesFile = modulesFile = new ModulesFile();
Module m = new Module("M");
parser.ast.Module m = new parser.ast.Module("M");
Declaration d = new Declaration("x", new DeclarationInt(Expression.Int(0), Expression.Int(numStates - 1)));
d.setStart(Expression.Int(0));
m.addDeclaration(d);
Expand Down
4 changes: 2 additions & 2 deletions prism/src/prism/Modules2MTBDD.java
Original file line number Diff line number Diff line change
Expand Up @@ -902,7 +902,7 @@ else if (sys instanceof SystemReference) {
private SystemDDs translateSystemModule(SystemModule sys, int[] synchMin) throws PrismException
{
SystemDDs sysDDs;
Module module;
parser.ast.Module module;
String synch;
int i, m;

Expand Down Expand Up @@ -1366,7 +1366,7 @@ else if (compDDs2.max > compDDs1.max) {
// translate a single module to a dd
// for a given synchronizing action ("" = none)

private ComponentDDs translateModule(int m, Module module, String synch, int synchMin) throws PrismException
private ComponentDDs translateModule(int m, parser.ast.Module module, String synch, int synchMin) throws PrismException
{
ComponentDDs compDDs;
JDDNode guardDDs[], upDDs[], tmp;
Expand Down
4 changes: 2 additions & 2 deletions prism/src/pta/DigitalClocks.java
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ public Object visit(Declaration e) throws PrismLangException
allInVariants = null;
mf = (ModulesFile) mf.accept(new ASTTraverseModify()
{
public Object visit(Module e) throws PrismLangException
public Object visit(parser.ast.Module e) throws PrismLangException
{
Command timeCommand;
Updates ups;
Expand Down Expand Up @@ -505,7 +505,7 @@ public void visitPost(ModulesFile e) throws PrismLangException
scaleFactor = computeGCD(allClockVals);
}

public void visitPre(Module e) throws PrismLangException
public void visitPre(parser.ast.Module e) throws PrismLangException
{
// Create new array to store clocks for this module
currentClockList = new ArrayList<String>();
Expand Down
16 changes: 8 additions & 8 deletions prism/src/pta/Modules2PTA.java
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ public Modules2PTA(PrismComponent parent, ModulesFile modulesFile) throws PrismE
public PTA translate() throws PrismLangException
{
int i, numModules;
Module module, moduleNew;
parser.ast.Module module, moduleNew;
ArrayList<String> nonClocks;
ArrayList<String> allNonClocks = new ArrayList<String>();
ArrayList<ArrayList<State>> pcStates;
Expand All @@ -85,15 +85,15 @@ public PTA translate() throws PrismLangException
// Check for inter-module variable references
modulesFile.accept(new ASTTraverse()
{
private Module inModule = null;
private parser.ast.Module inModule = null;

public void visitPre(Module e) throws PrismLangException
public void visitPre(parser.ast.Module e) throws PrismLangException
{
// Register the fact we are entering a module
inModule = e;
}

public void visitPost(Module e) throws PrismLangException
public void visitPost(parser.ast.Module e) throws PrismLangException
{
// Register the fact we are leaving a module
inModule = null;
Expand Down Expand Up @@ -165,7 +165,7 @@ public void visitPost(ExpressionVar e) throws PrismLangException
* Translate a single module.
* (Which has been transformed using convertModuleToPCForm)
*/
private PTA translateModule(Module module, ArrayList<State> pcStates) throws PrismLangException
private PTA translateModule(parser.ast.Module module, ArrayList<State> pcStates) throws PrismLangException
{
// Clocks and PC variable stuff
ArrayList<String> clocks;
Expand Down Expand Up @@ -486,15 +486,15 @@ else if (expr2.getType() instanceof TypeClock) {
* @param pcVars: The variables that should be converted to a PC.
* @param pcStates: An empty ArrayList into which PC value states will be stored.
*/
private Module convertModuleToPCForm(Module module, List<String> pcVars, ArrayList<State> pcStates) throws PrismLangException
private parser.ast.Module convertModuleToPCForm(parser.ast.Module module, List<String> pcVars, ArrayList<State> pcStates) throws PrismLangException
{
// Info about variables in model to be used as program counter
int pcNumVars;
State pcInit;
// info about new program counter var
String pc;
// Components of old and new module
Module moduleNew;
parser.ast.Module moduleNew;
Declaration decl, declNew;
Command command, commandNew;
Expression guard, guardNew;
Expand Down Expand Up @@ -545,7 +545,7 @@ private Module convertModuleToPCForm(Module module, List<String> pcVars, ArrayLi
}

// Create a new module
moduleNew = new Module(module.getName());
moduleNew = new parser.ast.Module(module.getName());

// Preserve alphabet of old module (might change if some commands are not enabled)
moduleNew.setAlphabet(module.getAllSynchs());
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ public int getGroupCount()
}

for (int m = 0; m < parsedModel.getNumModules(); m++) {
Module module = parsedModel.getModule(m);
parser.ast.Module module = parsedModel.getModule(m);
for (int v = 0; v < module.getNumDeclarations(); v++) {
if (varNames.contains(module.getDeclaration(v).getName())) {
groupCount++;
Expand Down Expand Up @@ -182,7 +182,7 @@ public String getGroupName(int groupIndex)
}

for (int m = 0; m < parsedModel.getNumModules(); m++) {
Module module = parsedModel.getModule(m);
parser.ast.Module module = parsedModel.getModule(m);
for (int v = 0; v < module.getNumDeclarations(); v++) {
if (varNames.contains(module.getDeclaration(v).getName())) {
if (groupCount == groupIndex) {
Expand Down Expand Up @@ -248,7 +248,7 @@ public String getGroupToolTip(int groupIndex)
}

for (int m = 0; m < parsedModel.getNumModules(); m++) {
Module module = parsedModel.getModule(m);
parser.ast.Module module = parsedModel.getModule(m);
for (int v = 0; v < module.getNumDeclarations(); v++) {
if (varNames.contains(module.getDeclaration(v).getName())) {
if (groupCount == groupIndex) {
Expand Down Expand Up @@ -336,7 +336,7 @@ public int getLastColumnOfGroup(int groupIndex)
}

for (int m = 0; m < parsedModel.getNumModules(); m++) {
Module module = parsedModel.getModule(m);
parser.ast.Module module = parsedModel.getModule(m);
boolean atLeastOne = false;

for (int v = 0; v < module.getNumDeclarations(); v++) {
Expand Down
4 changes: 2 additions & 2 deletions prism/src/userinterface/simulator/SimulationView.java
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ public void refreshToDefaultView(boolean pathActive, ModulesFile parsedModel)
canUseCurrentView = false;
}
for (int m = 0; m < parsedModel.getNumModules(); m++) {
Module module = parsedModel.getModule(m);
parser.ast.Module module = parsedModel.getModule(m);
for (int v = 0; v < module.getNumDeclarations(); v++) {
if (!allVarNames.remove(module.getDeclaration(v).getName()))
canUseCurrentView = false;
Expand Down Expand Up @@ -275,7 +275,7 @@ public void refreshToDefaultView(boolean pathActive, ModulesFile parsedModel)
i++;
}
for (int m = 0; m < parsedModel.getNumModules(); m++) {
Module module = parsedModel.getModule(m);
parser.ast.Module module = parsedModel.getModule(m);
for (int v = 0; v < module.getNumDeclarations(); v++) {
visibleVariables.add(new Variable(i, module.getDeclaration(v).getName(), module.getDeclaration(v).getType()));
i++;
Expand Down