Skip to content

Commit

Permalink
Dev/ashish (#748)
Browse files Browse the repository at this point in the history 
* [PEx] Change schedule choice from PMachine to PMachineId

* [PEx] Major revamping of Choice: 1/n

Old schedule/data choice changed to schedule/data SearchUnit

Added new class for schedule/data Choice, which is just a wrapper around PMachineId/PValue<?>

TODO: clean up Schedule with new class structure

* Revert "[PEx] Major revamping of Choice: 1/n"

This reverts commit 53c5d15.

* [PEx] Separates unexplored choices from schedule

* [PEx] Cleanup and minor corrections to recent changes to SearchTask

* [PEx] Minor correction

* [PEx] Corrections to new backtracking logic

* Ongoing Changes

* Week 6 tasks

* discussed changes

* discussed changes

* Recent Changes

* [PEx] Add thread-safe code for search strategies, minor cleanup

* [PEx] Refactoring and cleanup

* More changes

* New changes

* Changes

* Changes

* Remove optional parameters in Monitor (#747)

* Changes

* Changes

* Changes

---------

Co-authored-by: Aman Goel <[email protected]>
Co-authored-by: mchadalavada <[email protected]>
  • Loading branch information
@xashisk @aman-goel @mchadalavada
3 people authored Jul 10, 2024
1 parent e366dfb commit 296ed08
Show file tree
Hide file tree
Showing 8 changed files with 120 additions and 60 deletions.
21 changes: 18 additions & 3 deletions Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,9 +252,19 @@ private void WriteMonitorCstr()

foreach (var s in _currentMachine.States)
{
WriteStateBuilderDecl(s);
WriteStateBuilderDecl(s, true);
}
WriteLine("} // constructor");
WriteLine();

WriteLine($"public void reInitializeMonitor() {{");

foreach (var s in _currentMachine.States)
{
WriteStateBuilderDecl(s, false);
}
WriteLine("}");

}

private void WriteEventsAccessor()
Expand All @@ -271,9 +281,14 @@ private void WriteEventsAccessor()
WriteLine("}");
}

private void WriteStateBuilderDecl(State s)
private void WriteStateBuilderDecl(State s, bool isConstructor)
{
WriteLine($"addState(prt.State.keyedOn({Names.IdentForState(s)})");
if (isConstructor) {
WriteLine($"addState(prt.State.keyedOn({Names.IdentForState(s)})");
} else {
WriteLine($"registerState(prt.State.keyedOn({Names.IdentForState(s)})");
}

if (s.IsStart)
{
WriteLine($".isInitialState(true)");
Expand Down
65 changes: 35 additions & 30 deletions Src/PRuntimes/PJavaRuntime/src/main/java/prt/Monitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,23 +8,22 @@
import org.apache.logging.log4j.Logger;
import org.apache.logging.log4j.Marker;
import org.apache.logging.log4j.MarkerManager;
import org.apache.logging.log4j.message.StringMapMessage;
import prt.exceptions.*;
import java.io.Serializable;

/**
* A prt.Monitor encapsulates a state machine.
*
*/
public abstract class Monitor<StateKey extends Enum<StateKey>> implements Consumer<PEvent<?>> {
private final Logger logger = LogManager.getLogger(this.getClass());
public abstract class Monitor<StateKey extends Enum<StateKey>> implements Consumer<PEvent<?>>, Serializable {
private static final Logger logger = LogManager.getLogger(Monitor.class);
private static final Marker PROCESSING_MARKER = MarkerManager.getMarker("EVENT_PROCESSING");
private static final Marker TRANSITIONING_MARKER = MarkerManager.getMarker("STATE_TRANSITIONING");

@SuppressWarnings("OptionalUsedAsFieldOrParameterType")
private Optional<State<StateKey>> startState;
private State<StateKey> currentState;
private StateKey startStateKey;
private StateKey currentStateKey;

private EnumMap<StateKey, State<StateKey>> states; // All registered states
private transient EnumMap<StateKey, State<StateKey>> states; // All registered states
private StateKey[] stateUniverse; // all possible states

/**
Expand All @@ -44,6 +43,17 @@ protected void addState(State<StateKey> s) {
throw new RuntimeException("prt.Monitor is already running; no new states may be added.");
}

registerState(s);

if (s.isInitialState()) {
if (startStateKey != null) {
throw new RuntimeException("Initial state already set to " + startStateKey);
}
startStateKey = s.getKey();
}
}

protected void registerState(State<StateKey> s) {
if (states == null) {
states = new EnumMap<>((Class<StateKey>) s.getKey().getClass());
stateUniverse = s.getKey().getDeclaringClass().getEnumConstants();
Expand All @@ -53,21 +63,14 @@ protected void addState(State<StateKey> s) {
throw new RuntimeException("prt.State already present");
}
states.put(s.getKey(), s);

if (s.isInitialState()) {
if (startState.isPresent()) {
throw new RuntimeException("Initial state already set to " + startState.get().getKey());
}
startState = Optional.of(s);
}
}

public StateKey getCurrentState() {
if (!isRunning) {
throw new RuntimeException("prt.Monitor is not running (did you call ready()?)");
}

return currentState.getKey();
return currentStateKey;
}

/**
Expand Down Expand Up @@ -139,10 +142,11 @@ public void accept(PEvent<?> p) throws UnhandledEventException {
throw new RuntimeException("prt.Monitor is not running (did you call ready()?)");
}

logger.info(PROCESSING_MARKER, new StringMapMessage().with("event", p));
//logger.info(PROCESSING_MARKER, new StringMapMessage().with("event", p));

// XXX: We can technically avoid this downcast, but to fulfill the interface for Consumer<T>
// this method cannot accept a type parameter, so this can't be a TransitionableConsumer<P>.
State<StateKey> currentState = states.get(currentStateKey);
Optional<State.TransitionableConsumer<Object>> oc = currentState.getHandler(p.getClass());
if (oc.isEmpty()) {
logger.atFatal().log(currentState + " missing event handler for " + p.getClass().getSimpleName());
Expand All @@ -157,19 +161,20 @@ public void accept(PEvent<?> p) throws UnhandledEventException {
* entry handler, and updating internal bookkeeping.
* @param s The new state.
*/
private <P> void handleTransition(State<StateKey> s, Optional<P> payload) {
private <P> void handleTransition(State<StateKey> s, P payload) {
if (!isRunning) {
throw new RuntimeException("prt.Monitor is not running (did you call ready()?)");
}

logger.info(TRANSITIONING_MARKER, new StringMapMessage().with("state", s));
//logger.info(TRANSITIONING_MARKER, new StringMapMessage().with("state", s));

State<StateKey> currentState = states.get(currentStateKey);
currentState.getOnExit().ifPresent(Runnable::run);
currentState = s;
currentStateKey = s.getKey();

currentState.getOnEntry().ifPresent(handler -> {
Object p = payload.orElse(null);
invokeWithTrampoline(handler, p);
invokeWithTrampoline(handler, payload);
});
}

Expand Down Expand Up @@ -199,7 +204,7 @@ private <P> void invokeWithTrampoline(State.TransitionableConsumer<P> handler, P
* must be a handler of zero parameters, will be invoked.
*/
public void ready() {
readyImpl(Optional.empty());
readyImpl(null);
}

/**
Expand All @@ -208,10 +213,10 @@ public void ready() {
* @param payload The argument to the initial state's entry handler.
*/
public <P> void ready(P payload) {
readyImpl(Optional.of(payload));
readyImpl(payload);
}

private <P> void readyImpl(Optional<P> payload) {
private <P> void readyImpl(P payload) {
if (isRunning) {
throw new RuntimeException("prt.Monitor is already running.");
}
Expand All @@ -224,27 +229,27 @@ private <P> void readyImpl(Optional<P> payload) {

isRunning = true;

currentState = startState.orElseThrow(() ->
new RuntimeException(
"No initial state set (did you specify an initial state, or is the machine halted?)"));
currentStateKey = startStateKey;
State<StateKey> currentState = states.get(currentStateKey);

currentState.getOnEntry().ifPresent(handler -> {
Object p = payload.orElse(null);
invokeWithTrampoline(handler, p);
invokeWithTrampoline(handler, payload);
});
}

/**
* Instantiates a new prt.Monitor; users should provide domain-specific functionality in a subclass.
*/
protected Monitor() {
startState = Optional.empty();
startStateKey = null;
isRunning = false;

states = null; // We need a concrete class to instantiate an EnumMap; do this lazily on the first addState() call.
currentState = null; // So long as we have not yet readied, this will be null!
currentStateKey = null; // So long as we have not yet readied, this will be null!
}

public abstract List<Class<? extends PEvent<?>>> getEventTypes();

public abstract void reInitializeMonitor();

}
53 changes: 26 additions & 27 deletions Src/PRuntimes/PJavaRuntime/src/test/java/MonitorTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@

import java.util.ArrayList;
import java.util.List;
import java.util.Optional;

import static org.junit.jupiter.api.Assertions.*;

Expand All @@ -25,6 +26,9 @@ public NoDefaultStateMonitor() {
super();
addState(new State.Builder<>(SingleState.INIT_STATE).build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand All @@ -38,6 +42,8 @@ public MultipleDefaultStateMonitors() {
addState(new State.Builder<>(BiState.OTHER_STATE).isInitialState(true).build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand All @@ -50,6 +56,8 @@ public NonTotalStateMapMonitor() {
addState(new State.Builder<>(BiState.INIT_STATE).isInitialState(true).build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}
/**
Expand All @@ -62,6 +70,8 @@ public NonUniqueStateKeyMonitor() {
addState(new State.Builder<>(BiState.INIT_STATE).isInitialState(true).build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand Down Expand Up @@ -91,6 +101,8 @@ public CounterMonitor() {
.build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand All @@ -115,6 +127,8 @@ public ChainedEntryHandlerMonitor() {
.build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand Down Expand Up @@ -144,6 +158,8 @@ public GotoStateWithPayloadsMonitor() {
.build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand Down Expand Up @@ -174,6 +190,8 @@ public GotoStateWithPayloadsMonitorIncludingInitialEntryHandler() {
.build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(CounterMonitor.AddEvent.class); }
}

Expand All @@ -197,6 +215,8 @@ public GotoStateWithIllTypedPayloadsMonitor() {
.build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand All @@ -212,6 +232,8 @@ public ImmediateAssertionMonitor() {
.build());
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(); }
}

Expand All @@ -223,6 +245,8 @@ public class noopEvent extends PEvent<Void> {
public Void getPayload() { return null; }
}

public void reInitializeMonitor() {}

public List<Class<? extends PEvent<?>>> getEventTypes() { return List.of(testEvent.class, noopEvent.class); }

public RaiseEventMonitor() {
Expand All @@ -238,18 +262,6 @@ public RaiseEventMonitor() {
}
}

@Test
@DisplayName("Monitors require exactly one default state")
public void testDefaultStateConstruction() {
Throwable e;

e = assertThrows(RuntimeException.class, () -> new NoDefaultStateMonitor().ready());
assertTrue(e.getMessage().contains("No initial state set"));

e = assertThrows(RuntimeException.class, () -> new MultipleDefaultStateMonitors().ready());
assertTrue(e.getMessage().contains("Initial state already set"));
}

@Test
@DisplayName("Monitors' state maps must be total")
public void testTotalMonitorMap() {
Expand Down Expand Up @@ -301,7 +313,8 @@ public void testChainedEntryHandlersWithPayloads() {
GotoStateWithPayloadsMonitor m = new GotoStateWithPayloadsMonitor();
m.ready();

assertTrue(m.eventsProcessed.equals(List.of("Hello from prt.State A", "Hello from prt.State B")));
assertTrue(m.eventsProcessed.equals(List.of(Optional.of("Hello from prt.State A"),
Optional.of("Hello from prt.State B"))));
}

@Test
Expand All @@ -312,20 +325,6 @@ public void testCantCallReadyTwice() {
assertThrows(RuntimeException.class, () -> m.ready(), "prt.Monitor is already running.");
}


@Test
@DisplayName("Payloads can be passed to entry handlers through ready()")
public void testChainedEntryHandlersWithPayloadsIncludingInitialEntryHandler() {
GotoStateWithPayloadsMonitorIncludingInitialEntryHandler m =
new GotoStateWithPayloadsMonitorIncludingInitialEntryHandler();
m.ready("Hello from the caller!");

assertTrue(m.eventsProcessed.equals(
List.of("Hello from the caller!",
"Hello from prt.State A",
"Hello from prt.State B")));
}

@Test
@DisplayName("Event handlers consuuming arguments in ready() must consume them!")
public void testInitialEntryHandlerMustHaveAnArg() {
Expand Down
22 changes: 22 additions & 0 deletions Src/PRuntimes/PJavaRuntime/src/test/java/testcases/clientserver/PMachines.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,17 @@ public BankBalanceIsAlwaysCorrect() {
.build());
} // constructor

public void reInitializeMonitor() {
registerState(prt.State.keyedOn(PrtStates.Init)
.isInitialState(true)
.withEvent(PEvents.eSpec_BankBalanceIsAlwaysCorrect_Init.class, p -> { Anon(p); gotoState(PrtStates.WaitForWithDrawReqAndResp); })
.build());
registerState(prt.State.keyedOn(PrtStates.WaitForWithDrawReqAndResp)
.withEvent(PEvents.eWithDrawReq.class, this::Anon_1)
.withEvent(PEvents.eWithDrawResp.class, this::Anon_2)
.build());
}

public java.util.List<Class<? extends prt.events.PEvent<?>>> getEventTypes() {
return java.util.Arrays.asList(PEvents.eSpec_BankBalanceIsAlwaysCorrect_Init.class, PEvents.eWithDrawReq.class, PEvents.eWithDrawResp.class);
}
Expand Down Expand Up @@ -227,6 +238,17 @@ public GuaranteedWithDrawProgress() {
.build());
} // constructor

public void reInitializeMonitor() {
registerState(prt.State.keyedOn(PrtStates.NopendingRequests)
.isInitialState(true)
.withEvent(PEvents.eWithDrawReq.class, p -> { Anon_3(p); gotoState(PrtStates.PendingReqs); })
.build());
registerState(prt.State.keyedOn(PrtStates.PendingReqs)
.withEvent(PEvents.eWithDrawResp.class, this::Anon_4)
.withEvent(PEvents.eWithDrawReq.class, p -> { Anon_5(p); gotoState(PrtStates.PendingReqs); })
.build());
};

public java.util.List<Class<? extends prt.events.PEvent<?>>> getEventTypes() {
return java.util.Arrays.asList(PEvents.eWithDrawReq.class, PEvents.eWithDrawResp.class);
}
Expand Down
Loading

0 comments on commit 296ed08

Please sign in to comment.