Skip to content

Commit

Permalink
Add files via upload
Browse files Browse the repository at this point in the history
  • Loading branch information
kevinlano authored Dec 18, 2024
1 parent ff314ff commit c84573b
Show file tree
Hide file tree
Showing 75 changed files with 68,862 additions and 0 deletions.
Binary file added version24/BAnyStatement.class
Binary file not shown.
85 changes: 85 additions & 0 deletions version24/BAnyStatement.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
import java.util.Vector;

/* Copyright K. Lano 2003-2013
Package: B AMN
*/

public class BAnyStatement extends BStatement
{ private Vector vars = new Vector(); // of String
private BExpression pred;
private BStatement code;

public BAnyStatement(Vector vs, BExpression qual,
BStatement body)
{ vars = vs;
pred = qual;
code = body;
}

public Vector getVars()
{ return vars; }

public BExpression getWhere()
{ return pred; }

public BStatement getThen()
{ return code; }

public Vector wr()
{ return code.wr(); }

public Vector rd()
{ Vector res = pred.rd();
res = VectorUtil.union(res,code.rd());
res.removeAll(vars);
return res;
}

public String toString()
{ String res = "ANY ";
for (int i = 0; i < vars.size(); i++)
{ String var = (String) vars.get(i);
res = res + var;
if (i < vars.size() - 1)
{ res = res + ", "; }
}
res = res + " WHERE " + pred + "\n" + " THEN " +
code + " END";
return res;
}

public BStatement substituteEq(String oldE, BExpression newE)
{ if (vars.contains(oldE)) { return this; }
BExpression npred = pred.substituteEq(oldE,newE);
BStatement ncode = code.substituteEq(oldE,newE);
return new BAnyStatement(vars,npred,ncode);
}

public BStatement simplify()
{ BExpression npred = pred.simplify();
BStatement ncode = code.simplify();
return new BAnyStatement(vars,npred,ncode);
}

public BStatement seq2parallel()
{ BStatement ncode = code.seq2parallel();
return new BAnyStatement(vars,pred,ncode);
}

public BStatement normalise()
{ BAnyStatement res;
BStatement stat = code.normalise();
if (stat instanceof BAnyStatement)
{ BAnyStatement inner = (BAnyStatement) stat;
Vector newvars = new Vector();
newvars.addAll(vars);
newvars.addAll(inner.getVars());
BExpression newpred = new BBinaryExpression("&",pred,inner.getWhere());
res = new BAnyStatement(newvars,newpred,inner.getThen());
}
else
{ res = new BAnyStatement(vars,pred,stat); }
return res;
}
}

Binary file added version24/BApplyExpression.class
Binary file not shown.
114 changes: 114 additions & 0 deletions version24/BApplyExpression.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
import java.util.Vector;

/* Copyright K. Lano 2003-2013
Package: B AMN */

public class BApplyExpression extends BExpression
{ private String function;
private BExpression func; // function = func.toString()
private BExpression arg; // may be list
private Vector args;

public BApplyExpression(String f, BExpression a)
{ function = f;
func = new BBasicExpression(f);
arg = a;
}

public BApplyExpression(BExpression f, BExpression a)
{ function = f + "";
func = f;
arg = a;
}

public BApplyExpression(BExpression f, Vector arglist)
{ function = f + "";
func = f;
args = arglist;
String argstring = "";
for (int i = 0; i < arglist.size(); i++)
{ argstring = argstring + arglist.get(i);
if (i < arglist.size() - 1)
{ argstring = argstring + ","; }
}
arg = new BBasicExpression(argstring);
}

public Vector rd()
{ Vector res = func.rd();
res = VectorUtil.union(res,arg.rd());
return res;
}

public String getFunction()
{ return function; }

public BExpression getArgument()
{ return arg; }

public void setMultiplicity(int m)
{ multiplicity = m; }

public boolean setValued()
{ if (multiplicity != ModelElement.ONE)
{ return true; }
else
{ return arg.setValued(); }
}

public BExpression simplify()
{ if (arg == null)
{ System.err.println("Function: " + function + " with null argument");
return null;
}

if (func instanceof BBinaryExpression) // (f <+ {x |-> b})(x) is b
{ BBinaryExpression bbe = (BBinaryExpression) func;
if (bbe.getOperator().equals("<+") && (bbe.getRight() instanceof BSetExpression))
{ BSetExpression update = (BSetExpression) bbe.getRight();
BExpression elem0 = update.getElement(0);
if (elem0 != null && (elem0 instanceof BBinaryExpression))
{ BBinaryExpression belem0 = (BBinaryExpression) elem0;
if (belem0.getOperator().equals("|->") && (arg + "").equals(belem0.getLeft() + ""))
{ return belem0.getRight(); }
}
}
}

BExpression sarg = arg.simplify();
if (sarg instanceof BSetExpression)
{ BSetExpression se = (BSetExpression) sarg;
if (se.isSingleton())
{ BExpression argp = se.getElement(0);
// Vector vv = new Vector();
BApplyExpression newapp = new BApplyExpression(func,argp);
newapp.setMultiplicity(multiplicity);
// vv.add(newapp);
// return new BSetExpression(vv);
return newapp;
} // f(set) is never meant for real in UML-RSDS
}
return
new BApplyExpression(func,sarg);
}

public BExpression substituteEq(String oldE, BExpression newE)
{ if (oldE.equals(toString()))
{ return newE; }
BExpression argE = arg.substituteEq(oldE,newE);
BExpression funcE = func.substituteEq(oldE,newE);
if (funcE instanceof BBasicExpression) {}
else
{ funcE.setBrackets(true); }
BExpression res = new BApplyExpression(funcE,argE);
res.setMultiplicity(multiplicity);
return res;
}

public String toString()
{ if (function == null)
{ return func + "(" + arg + ")"; }
return function + "(" + arg + ")";
}
}

Binary file added version24/BApplySetExpression.class
Binary file not shown.
79 changes: 79 additions & 0 deletions version24/BApplySetExpression.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
import java.util.Vector;

public class BApplySetExpression extends BExpression
{ private String function;
private BExpression func;
private BExpression arg;

public BApplySetExpression(String f, BExpression a)
{ function = f;
func = new BBasicExpression(f);
arg = a;
}

public BApplySetExpression(BExpression f, BExpression a)
{ func = f;
function = "" + f;
arg = a;
}

public Vector rd()
{ Vector res = new Vector();
res.addAll(func.rd());
return VectorUtil.union(res,arg.rd());
}

public boolean setValued()
{ return true; }

public void setMultiplicity(int m)
{ multiplicity = m; }

public BExpression simplify()
{ BExpression sa = arg.simplify();
if (sa instanceof BSetExpression)
{ BSetExpression se = (BSetExpression) sa;
if (se.isSingleton())
{ BExpression arg1 = se.getElement(0);
Vector rr = new Vector();
if (arg1.setValued())
{ // f[{arg1}] is f[arg]
BApplySetExpression newaps = new BApplySetExpression(func,arg1);
newaps.setMultiplicity(multiplicity);
if (multiplicity == ModelElement.ONE)
{ return newaps; }
else
{ return new BUnaryExpression("union",newaps); }
} // else, its {f(arg1)}
BApplyExpression ap =
new BApplyExpression(func,arg1);
ap.setMultiplicity(multiplicity);
// if (multiplicity == ModelElement.ONE)
// {
rr.add(ap);
return new BSetExpression(rr);
// } // or just ap if setValued anyway
// else
// { return ap; }
}
else if (se.isEmpty())
{ return new BSetExpression(new Vector()); }
}
BApplySetExpression res = new BApplySetExpression(func,sa);
res.setMultiplicity(multiplicity);
return res;
}

public String toString()
{ return function + "[" + arg + "]"; }

public BExpression substituteEq(String oldE, BExpression newE)
{ if (oldE.equals(toString()))
{ return newE; }
BExpression argE = arg.substituteEq(oldE,newE);
BExpression res = new BApplySetExpression(function,argE);
res.setMultiplicity(multiplicity);
return res;
}
} // and in func

Binary file added version24/BAssignStatement.class
Binary file not shown.
96 changes: 96 additions & 0 deletions version24/BAssignStatement.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
import java.util.Vector;

/* Copyright K. Lano 2003-2013
Package: B AMN
*/

public class BAssignStatement extends BStatement
{ private BExpression lhs;
private BExpression rhs;

public BAssignStatement(BExpression l, BExpression r)
{ lhs = l;
rhs = r;
}

public BExpression getRhs()
{ return rhs; }

public BExpression getLhs()
{ return lhs; }

public String toString()
{ return lhs + " := " + rhs; }

public BStatement substituteEq(String oldE, BExpression newE)
{ // BExpression nlhs = lhs.substituteEq(oldE,newE);
BExpression nrhs = rhs.substituteEq(oldE,newE);
return new BAssignStatement(lhs,nrhs);
}

public BStatement simplify()
{ // BExpression nlhs = lhs.substituteEq(oldE,newE);
BExpression nrhs = rhs.simplify();
return new BAssignStatement(lhs,nrhs);
}

public Vector wr()
{ Vector res = new Vector();

if (lhs instanceof BBasicExpression)
{ res.add(lhs + "");
return res;
}
if (lhs instanceof BApplyExpression)
{ BApplyExpression bae = (BApplyExpression) lhs;
String f = bae.getFunction();
res.add(f);
return res;
}
return res;
}

public Vector rd()
{ Vector res = new Vector();
res.addAll(rhs.rd());

if (lhs instanceof BBasicExpression)
{ return res; }

if (lhs instanceof BApplyExpression)
{ BApplyExpression bae = (BApplyExpression) lhs;
BExpression arg = bae.getArgument();
res = VectorUtil.union(res,arg.rd());
return res;
}
return res;
}

public BStatement seq2parallel()
{ return this; }

public BStatement normalise()
{ if (lhs instanceof BBasicExpression)
{ return this; }
if (lhs instanceof BApplyExpression)
{ BApplyExpression bae = (BApplyExpression) lhs;
String f = bae.getFunction();
BExpression arg = bae.getArgument();

BExpression maplet =
new BBinaryExpression("|->",arg,rhs);
BSetExpression bse =
new BSetExpression();
bse.addElement(maplet);
BExpression newlhs =
new BBasicExpression(f);
BExpression newrhs =
new BBinaryExpression("<+",newlhs,bse);
newrhs.setBrackets(true);
return new BAssignStatement(newlhs,newrhs);
}
return this;
}

}

Binary file added version24/BBasicExpression.class
Binary file not shown.
Loading

0 comments on commit c84573b

Please sign in to comment.