PLCgen: event loop counter bound calculation
Problem
The code generator uses a while-loop to check for available events. To ensure that the PLC is fast enough, it would be nice to know how often this loop is executed.
Proposed solution
Conceptually, you search the state space for sequences of controllable events. By keeping track of the ends of these sequences, you can keep appending controllable events until the set of states is invariant. When this happens, the longest sequence is found if the set of states is empty, or finite response is disproved if the set is non-empty. Below, a snippet of Java-code is given, based on the synthesis algorithm, which does this.
Code
private static void checkControllableSequence(SynthesisAutomaton aut, boolean dbgEnabled) {
// Build a list of edges for controllable events.
List<SynthesisEdge> controllableEdges = list();
for (Entry<Event, List<SynthesisEdge>> entry : aut.eventEdges.entrySet()) {
if (entry.getKey().getControllable()) {
controllableEdges.addAll(entry.getValue());
}
}
// Find all reachable states.
CifDataSynthesisReachability reachability = new CifDataSynthesisReachability(aut, 0, //
"forward controlled-behavior", "initialization", "controlled-behavior", //
aut.ctrlBeh, // no restriction
false, // not bad states = good states
true, // forward reachability
true, true, // include all edges
dbgEnabled);
BDD sequenceStates = reachability.performReachability(aut.initialCtrl.id());
// Iterate over the sequence.
for (int maxSequence = 0;; maxSequence++) {
dbg("Iteration " + maxSequence);
// Build the set of states after n + 1 sequential controllable transitions.
BDD newStates = aut.factory.zero();
for (SynthesisEdge edge : controllableEdges) {
// Take a controllable transition to a (new) state.
edge.preApply(true, null);
BDD edgeStates = edge.apply(sequenceStates.id(), false, true, null, false);
edge.postApply(true);
newStates.orWith(edgeStates);
}
// If there are no states remaining, we have found the longest sequence.
if (newStates.isZero()) {
dbg("Controlled system has at most %d consecutive controllable events.", maxSequence);
return;
}
// If there is no change, we have found one or more cycles.
if (newStates.equalsBDD(sequenceStates)) {
dbg("Controlled system does not have finite response.");
return;
}
// Update end states of the sequence.
sequenceStates = newStates;
// Stop if requested.
if (aut.env.isTerminationRequested()) {
return;
}
}
}
Notes/future improvements
Some initial tests show that this computation is feasible, taking up to a few minutes for a random lock model. My tests were done by replacing the main data-based synthesis method (synthesizeFixedPoints
) with the method above. This brings with it a lot of irrelevant code, so it might be faster if this is properly implemented.
I tried to get some useful output when the system does not have finite response, to give the designer some input on which events might cause this. However, this method does not find minimal cycles, so it is hard to separate the problematic events from other enabled events.
If used in combination with sequencing, the performance can probably be improved. Because you only care about controllable events within an event loop in the generated code.