Skip to content

Commit

Permalink
[PExplicit] Uniquify instanceId for PMachine as well as PMonitor
Browse files Browse the repository at this point in the history
  • Loading branch information
aman-goel committed Apr 22, 2024
1 parent 1ae4482 commit e290af6
Show file tree
Hide file tree
Showing 4 changed files with 31 additions and 16 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,9 @@ public static PMachine getGlobalMachine(Class<? extends PMachine> type, int idx)
if (idx >= machinesOfType.size()) {
return null;
}
return machineListByType.get(type).get(idx);
PMachine result = machineListByType.get(type).get(idx);
assert (machineSet.contains(result));
return result;
}

/**
Expand All @@ -81,6 +83,7 @@ public static void addGlobalMachine(PMachine machine, int machineCount) {
if (!machineListByType.containsKey(machine.getClass())) {
machineListByType.put(machine.getClass(), new ArrayList<>());
}
assert (machineCount == machineListByType.get(machine.getClass()).size());
machineListByType.get(machine.getClass()).add(machine);
machineSet.add(machine);
assert (machineListByType.get(machine.getClass()).get(machineCount) == machine);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -24,11 +24,9 @@
* Represents the base class for all P machines.
*/
public abstract class PMachine implements Serializable, Comparable<PMachine> {
@Getter
private static final int mainMachineId = 2;
@Getter
private static final Map<String, PMachine> nameToMachine = new HashMap<>();
protected static int globalMachineId = mainMachineId;
protected static int globalMachineId = 1;
@Getter
protected final int typeId;
@Getter
Expand All @@ -40,6 +38,11 @@ public abstract class PMachine implements Serializable, Comparable<PMachine> {
private final DeferQueue deferQueue;
@Getter
private final Map<String, PContinuation> continuationMap = new TreeMap<>();
/**
* Unique identifier across all PMachines/PMonitors
* For PMachines, instanceId runs from 1 to #PMachines
* For PMonitors, instanceId runs from -1 to -#PMonitors
*/
@Getter
protected int instanceId;
@Getter
Expand Down Expand Up @@ -68,7 +71,7 @@ public abstract class PMachine implements Serializable, Comparable<PMachine> {
public PMachine(String name, int id, State startState, State... states) {
// initialize name, ids
this.name = name;
this.instanceId = globalMachineId++;
this.instanceId = ++globalMachineId;
this.typeId = id;
nameToMachine.put(toString(), this);

Expand Down Expand Up @@ -528,14 +531,15 @@ public void enterNewState(State newState, PValue<?> payload) {

@Override
public int compareTo(PMachine rhs) {
return (this.hashCode() - rhs.hashCode());
if (rhs == null) {
return this.instanceId;
}
return (this.instanceId - rhs.instanceId);
}

@Override
public int hashCode() {
if (name == null)
return instanceId ^ typeId;
return name.hashCode() ^ instanceId ^ typeId;
return this.instanceId;
}

@Override
Expand All @@ -545,13 +549,10 @@ else if (!(obj instanceof PMachine)) {
return false;
}
if (this.name == null) {
return (((PMachine) obj).name == null)
&& this.instanceId == (((PMachine) obj).instanceId)
&& this.typeId == (((PMachine) obj).typeId);
}
return (((PMachine) obj).name == null);
}
return this.name.equals(((PMachine) obj).name)
&& this.instanceId == (((PMachine) obj).instanceId)
&& this.typeId == (((PMachine) obj).typeId);
&& this.instanceId == (((PMachine) obj).instanceId);
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,12 @@
* Represents a P monitor.
*/
public class PMonitor extends PMachine {
/**
* Global monitor id
* Runs from -(#Monitors) to 0
*/
protected static int globalMonitorId = 0;

/**
* Monitor constructor
*
Expand All @@ -14,8 +20,8 @@ public class PMonitor extends PMachine {
*/
public PMonitor(String name, int id, State startState, State... states) {
super(name, id, startState, states);
this.instanceId = 0;
globalMachineId--;
this.instanceId = --globalMonitorId;
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@

import lombok.Getter;
import pexplicit.runtime.machine.PMachine;
import pexplicit.runtime.machine.PMonitor;
import pexplicit.utils.exceptions.BugFoundException;

/**
* Represents the PValue for P machine
Expand All @@ -25,6 +27,9 @@ public PMachineValue(PMachine val) {
* @return unique machine instance id
*/
public int getId() {
if (value instanceof PMonitor) {
throw new BugFoundException(String.format("Cannot fetch id from a PMonitor: %s", value));
}
return value.getInstanceId();
}

Expand Down

0 comments on commit e290af6

Please sign in to comment.