Skip to content

Commit

Permalink
Fixed door returns int not boolean
Browse files Browse the repository at this point in the history
  • Loading branch information
@Tarrasch
Tarrasch committed Feb 18, 2011
1 parent 8b8bcf2 commit b348378
Show file tree
Hide file tree
Showing 5 changed files with 70 additions and 73 deletions.
37 changes: 20 additions & 17 deletions Door.jr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,19 +6,21 @@ import java.util.ArrayList;
public class Door {

private ArrayList<Person> entrants;
private boolean isLocked;
private int landlordCalls;
private cap void() returnOkCap;



public op boolean add(Person p);
public op int add(Person p);
public op boolean isClosed();
public op ArrayList<Person> lock(cap void() returnOkCap);
public op List<Person> lock(cap void() returnOkCap);
public cap List<Person>(cap void() returnOkCap) lastCall = lock;
public op void leave(Person p);


public Door() {
entrants = new ArrayList<Person>();
isLocked = false;
landlordCalls = 0;
Global.door = this;

}
Expand All @@ -38,40 +40,39 @@ public class Door {
{
inni ArrayList<Person> lock(cap void() returnOkCap)
{
isLocked = true;
this.returnOkCap = returnOkCap;

landlordCalls++;
this.returnOkCap = returnOkCap;
return new ArrayList<Person>(entrants); // This adds stupid warning

}
[] boolean add(Person p)
[] int add(Person p)
{
asserts(!entrants.contains(p), "Person " + p + " has already entered door");
if(isLocked)
if(landlordCalls < 2)
{
return false;
addPersonToList(p);

}
addPersonToList(p);
return true;
return landlordCalls;

}
[] void leave(Person p)
{
removePersonFromList(p);
if(isLocked && entrants.size() <= 2)
if(entrants.size() <= 2 && returnOkCap != null)
{
// Ok, only landlord (or ll+assistant) should be left, lets notift him
// Ok, only landlord (or ll+assistant) should be left, lets notify him
send returnOkCap();
}
if(isLocked && entrants.size() == 0)
if(entrants.size() == 0)
{
// Ok, now even landlord left, lets exit gracfully
break;
}
}
[] boolean isClosed()
{
return isLocked;
return landlordCalls >= 2;
}
}
}
Expand Down Expand Up @@ -108,6 +109,7 @@ public class Door {
***************************************************/
public static void main(String[] args) {
allDoorTests();

}

public static void allDoorTests()
Expand Down Expand Up @@ -170,7 +172,8 @@ public class Door {
TestPerson landlord = new TestPerson(); // this emulates Landlord (auto-enters)
JR.nap(100);
op void returnCap(); // The landlords replyChannel
ArrayList<Person> list = d.lock(returnCap);
List<Person> list = d.lastCall(returnCap);
list = d.lock(returnCap); // Now we must close
asserts(list != d.entrants, "Should not be reference to entrants!");
asserts(list.equals(d.entrants), "Should however be equal to entrants!");

Expand Down
3 changes: 2 additions & 1 deletion Person.jr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,8 @@ public abstract class Person {

private boolean enterDoor()
{
return Global.door.add(this);
numCalls = Global.door.add(this);
return numCalls < 2;
}

private void leaveBar()
Expand Down
67 changes: 29 additions & 38 deletions jrGen/Door.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,15 @@
public class Door extends java.lang.Object {
{ JRinit(); }
private ArrayList entrants;
private boolean isLocked;
private int landlordCalls;
private // NUMBER 8
Cap_ext_ returnOkCap;
public Op_ext.JRProxyOp JRget_op_add_PersonToboolean()
public Op_ext.JRProxyOp JRget_op_add_PersonToint()
{
return op_add_PersonToboolean;
return op_add_PersonToint;
}

public Op_ext.JRProxyOp op_add_PersonToboolean;
public Op_ext.JRProxyOp op_add_PersonToint;

public Op_ext.JRProxyOp JRget_op_isClosed_voidToboolean()
{
Expand All @@ -31,13 +31,15 @@ public Op_ext.JRProxyOp JRget_op_isClosed_voidToboolean()

public Op_ext.JRProxyOp op_isClosed_voidToboolean;

public Op_ext.JRProxyOp JRget_op_lock_Cap_voidTovoidTojavadotutildotArrayList()
public Op_ext.JRProxyOp JRget_op_lock_Cap_voidTovoidTojavadotutildotList()
{
return op_lock_Cap_voidTovoidTojavadotutildotArrayList;
return op_lock_Cap_voidTovoidTojavadotutildotList;
}

public Op_ext.JRProxyOp op_lock_Cap_voidTovoidTojavadotutildotArrayList;
public Op_ext.JRProxyOp op_lock_Cap_voidTovoidTojavadotutildotList;

public // NUMBER 8
Cap_ext_ lastCall = new Cap_ext_(JRget_op_lock_Cap_voidTovoidTojavadotutildotList());
public Op_ext.JRProxyOp JRget_op_leave_PersonTovoid()
{
return op_leave_PersonTovoid;
Expand All @@ -52,7 +54,7 @@ public Door() {
// Begin Expr2
entrants = new ArrayList();
// Begin Expr2
isLocked = false;
landlordCalls = 0;
// Begin Expr2
Global.door = this;
JRprocess();
Expand Down Expand Up @@ -248,8 +250,8 @@ private void startLoop() {
JRLoop14: while (true) {
{
// Inni Statement without quantifier
JRInstmt6.armArray[0] = new QuantRec(new Cap_ext_(op_lock_Cap_voidTovoidTojavadotutildotArrayList, "java.util.ArrayList<Person>"), 0, 0);
JRInstmt6.armArray[1] = new QuantRec(new Cap_ext_(op_add_PersonToboolean, "boolean"), 1, 1);
JRInstmt6.armArray[0] = new QuantRec(new Cap_ext_(op_lock_Cap_voidTovoidTojavadotutildotList, "java.util.List<Person>"), 0, 0);
JRInstmt6.armArray[1] = new QuantRec(new Cap_ext_(op_add_PersonToint, "int"), 1, 1);
JRInstmt6.armArray[2] = new QuantRec(new Cap_ext_(op_leave_PersonTovoid, "void"), 2, 2);
JRInstmt6.armArray[3] = new QuantRec(new Cap_ext_(op_isClosed_voidToboolean, "boolean"), 3, 3);
JRInstmt6.lock();
Expand Down Expand Up @@ -304,7 +306,7 @@ private void startLoop() {
try {
{
// Begin Expr2
isLocked = true;
landlordCalls++;
// Begin Expr2
this.returnOkCap = returnOkCap;
// Return
Expand All @@ -313,7 +315,7 @@ private void startLoop() {
{ if (JRrrecv6.retOp != null)
JRrrecv6.retOp.send(jrvm.getTimestamp(), (edu.ucdavis.jr.RemoteHandler) null, new java.lang.Object [] {(new ArrayList(entrants))});
else {
java.util.ArrayList JRevaltmp = new ArrayList(entrants);
java.util.List JRevaltmp = new ArrayList(entrants);

}
break _label_JRInstmt6; }}
Expand Down Expand Up @@ -397,30 +399,17 @@ else if ((JRrrecv6.handler != null) && !(JRe instanceof java.rmi.RemoteException
{
// Begin Expr2
asserts(!entrants.contains(p), "Person " + p + " has already entered door");
if (isLocked) {
// Return
{
if (true)
{ if (JRrrecv6.retOp != null)
JRrrecv6.retOp.send(jrvm.getTimestamp(), (edu.ucdavis.jr.RemoteHandler) null, new java.lang.Object [] {(boolean)(false)});
else {
boolean JRevaltmp = false;

}
break _label_JRInstmt6; }}

// End Return

if (landlordCalls < 2) {
// Begin Expr2
addPersonToList(p);
}
// Begin Expr2
addPersonToList(p);
// Return
{
if (true)
{ if (JRrrecv6.retOp != null)
JRrrecv6.retOp.send(jrvm.getTimestamp(), (edu.ucdavis.jr.RemoteHandler) null, new java.lang.Object [] {(boolean)(true)});
JRrrecv6.retOp.send(jrvm.getTimestamp(), (edu.ucdavis.jr.RemoteHandler) null, new java.lang.Object [] {(int)(landlordCalls)});
else {
boolean JRevaltmp = true;
int JRevaltmp = landlordCalls;

}
break _label_JRInstmt6; }}
Expand Down Expand Up @@ -504,10 +493,10 @@ else if ((JRrrecv6.handler != null) && !(JRe instanceof java.rmi.RemoteException
{
// Begin Expr2
removePersonFromList(p);
if (isLocked && entrants.size() <= 2) {
if (entrants.size() <= 2 && returnOkCap != null) {
returnOkCap.send(jrvm.getTimestamp(), (edu.ucdavis.jr.RemoteHandler) null, (java.lang.Object[]) null);
}
if (isLocked && entrants.size() == 0) {
if (entrants.size() == 0) {
{ if (JRrrecv6.retOp != null)
JRrrecv6.retOp.send(jrvm.getTimestamp(), (java.lang.Object []) null);
break JRLoop14;}
Expand Down Expand Up @@ -588,9 +577,9 @@ else if ((JRrrecv6.handler != null) && !(JRe instanceof java.rmi.RemoteException
{
if (true)
{ if (JRrrecv6.retOp != null)
JRrrecv6.retOp.send(jrvm.getTimestamp(), (edu.ucdavis.jr.RemoteHandler) null, new java.lang.Object [] {(boolean)(isLocked)});
JRrrecv6.retOp.send(jrvm.getTimestamp(), (edu.ucdavis.jr.RemoteHandler) null, new java.lang.Object [] {(boolean)(landlordCalls >= 2)});
else {
boolean JRevaltmp = isLocked;
boolean JRevaltmp = landlordCalls >= 2;

}
break _label_JRInstmt6; }}
Expand Down Expand Up @@ -741,7 +730,9 @@ public static void testDoor() {
} catch (Exception e) { throw new jrRuntimeError("Cannot initialize op"); }


ArrayList list = ((java.util.ArrayList) (new Cap_ext_(d.JRget_op_lock_Cap_voidTovoidTojavadotutildotArrayList(), "java.util.ArrayList")).call(jrvm.getTimestamp(), new java.lang.Object [] {new Cap_ext_(op_returnCap_voidTovoid)}));
List list = ((java.util.List) (new Cap_ext_(d.lastCall, "java.util.List")).call(jrvm.getTimestamp(), new java.lang.Object [] {new Cap_ext_(op_returnCap_voidTovoid)}));
// Begin Expr2
list = ((java.util.List) (new Cap_ext_(d.JRget_op_lock_Cap_voidTovoidTojavadotutildotList(), "java.util.List")).call(jrvm.getTimestamp(), new java.lang.Object [] {new Cap_ext_(op_returnCap_voidTovoid)}));
// Begin Expr2
asserts(list != d.entrants, "Should not be reference to entrants!");
// Begin Expr2
Expand Down Expand Up @@ -1017,15 +1008,15 @@ protected void JRinit() {
op_doorProcess_voidTovoid = new Op_ext_.JRProxyOp(new ProcOp_voidTovoid_impldoorProcess(this));
op_leave_PersonTovoid =
new Op_ext_.JRProxyOp(new InOp_ext_impl());
op_lock_Cap_voidTovoidTojavadotutildotArrayList =
op_lock_Cap_voidTovoidTojavadotutildotList =
new Op_ext_.JRProxyOp(new InOp_ext_impl());
op_isClosed_voidToboolean =
new Op_ext_.JRProxyOp(new InOp_ext_impl());
op_add_PersonToboolean =
op_add_PersonToint =
new Op_ext_.JRProxyOp(new InOp_ext_impl());
} catch (Exception JRe)
{ throw new jrRuntimeError(JRe.toString()); }
jrresref = new JRDoor(op_doorProcess_voidTovoid, op_leave_PersonTovoid, op_lock_Cap_voidTovoidTojavadotutildotArrayList, op_isClosed_voidToboolean, op_add_PersonToboolean);
jrresref = new JRDoor(op_doorProcess_voidTovoid, op_leave_PersonTovoid, op_lock_Cap_voidTovoidTojavadotutildotList, op_isClosed_voidToboolean, op_add_PersonToint);
this.JRcalled = true;
}
private boolean JRproc = false;
Expand Down
32 changes: 16 additions & 16 deletions jrGen/JRDoor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,12 +27,12 @@ public void JRset_op_leave_PersonTovoid(Cap_ext_ op_leave_PersonTovoid) {
this.op_leave_PersonTovoid = op_leave_PersonTovoid;
}

public Cap_ext_ op_lock_Cap_voidTovoidTojavadotutildotArrayList;
public Cap_ext_ JRget_op_lock_Cap_voidTovoidTojavadotutildotArrayList() {
return op_lock_Cap_voidTovoidTojavadotutildotArrayList;
public Cap_ext_ op_lock_Cap_voidTovoidTojavadotutildotList;
public Cap_ext_ JRget_op_lock_Cap_voidTovoidTojavadotutildotList() {
return op_lock_Cap_voidTovoidTojavadotutildotList;
}
public void JRset_op_lock_Cap_voidTovoidTojavadotutildotArrayList(Cap_ext_ op_lock_Cap_voidTovoidTojavadotutildotArrayList) {
this.op_lock_Cap_voidTovoidTojavadotutildotArrayList = op_lock_Cap_voidTovoidTojavadotutildotArrayList;
public void JRset_op_lock_Cap_voidTovoidTojavadotutildotList(Cap_ext_ op_lock_Cap_voidTovoidTojavadotutildotList) {
this.op_lock_Cap_voidTovoidTojavadotutildotList = op_lock_Cap_voidTovoidTojavadotutildotList;
}

public Cap_ext_ op_isClosed_voidToboolean;
Expand All @@ -43,39 +43,39 @@ public void JRset_op_isClosed_voidToboolean(Cap_ext_ op_isClosed_voidToboolean)
this.op_isClosed_voidToboolean = op_isClosed_voidToboolean;
}

public Cap_ext_ op_add_PersonToboolean;
public Cap_ext_ JRget_op_add_PersonToboolean() {
return op_add_PersonToboolean;
public Cap_ext_ op_add_PersonToint;
public Cap_ext_ JRget_op_add_PersonToint() {
return op_add_PersonToint;
}
public void JRset_op_add_PersonToboolean(Cap_ext_ op_add_PersonToboolean) {
this.op_add_PersonToboolean = op_add_PersonToboolean;
public void JRset_op_add_PersonToint(Cap_ext_ op_add_PersonToint) {
this.op_add_PersonToint = op_add_PersonToint;
}

public JRDoor(JRDoor copy)
{
this.op_doorProcess_voidTovoid = copy.op_doorProcess_voidTovoid;
this.op_leave_PersonTovoid = copy.op_leave_PersonTovoid;
this.op_lock_Cap_voidTovoidTojavadotutildotArrayList = copy.op_lock_Cap_voidTovoidTojavadotutildotArrayList;
this.op_lock_Cap_voidTovoidTojavadotutildotList = copy.op_lock_Cap_voidTovoidTojavadotutildotList;
this.op_isClosed_voidToboolean = copy.op_isClosed_voidToboolean;
this.op_add_PersonToboolean = copy.op_add_PersonToboolean;
this.op_add_PersonToint = copy.op_add_PersonToint;

}
public JRDoor(Object ... opSig)
{
this.op_doorProcess_voidTovoid = new Cap_ext_((Op_ext_.JRProxyOp)opSig[0]);
this.op_leave_PersonTovoid = new Cap_ext_((Op_ext_.JRProxyOp)opSig[1]);
this.op_lock_Cap_voidTovoidTojavadotutildotArrayList = new Cap_ext_((Op_ext_.JRProxyOp)opSig[2]);
this.op_lock_Cap_voidTovoidTojavadotutildotList = new Cap_ext_((Op_ext_.JRProxyOp)opSig[2]);
this.op_isClosed_voidToboolean = new Cap_ext_((Op_ext_.JRProxyOp)opSig[3]);
this.op_add_PersonToboolean = new Cap_ext_((Op_ext_.JRProxyOp)opSig[4]);
this.op_add_PersonToint = new Cap_ext_((Op_ext_.JRProxyOp)opSig[4]);

}
public JRDoor(boolean dummy) {
super(dummy);
this.op_doorProcess_voidTovoid = Cap_ext_.noop;
this.op_leave_PersonTovoid = Cap_ext_.noop;
this.op_lock_Cap_voidTovoidTojavadotutildotArrayList = Cap_ext_.noop;
this.op_lock_Cap_voidTovoidTojavadotutildotList = Cap_ext_.noop;
this.op_isClosed_voidToboolean = Cap_ext_.noop;
this.op_add_PersonToboolean = Cap_ext_.noop;
this.op_add_PersonToint = Cap_ext_.noop;

}
public Object clone()
Expand Down
4 changes: 3 additions & 1 deletion jrGen/Person.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,10 @@ public void say(String msg) {
}

private boolean enterDoor() {
// Begin Expr2
numCalls = ((Integer) (new Cap_ext_(Global.door.JRget_op_add_PersonToint(), "int")).call(jrvm.getTimestamp(), new java.lang.Object [] {this}));
// Return
return (((Boolean) (new Cap_ext_(Global.door.JRget_op_add_PersonToboolean(), "boolean")).call(jrvm.getTimestamp(), new java.lang.Object [] {this})));
return (numCalls < 2);
// End Return

}
Expand Down

0 comments on commit b348378

Please sign in to comment.