Learning a model from a real system (Miniature Lift)

[Teck Ping Khoo]

Hi everyone

I have a real miniature lift with four levels. This lift is controlled by a PLC which can run a TCP server. I can set up a TCP client to connect to it and send commands to trigger inputs. The system will reply with its sensor and actuator states. The inputs are the button presses and an example of outputs is the level sensor (high when the lift car is level with any floor, low otherwise). The PLC can be easily reset by command. 

I wish to use learnlib to perform active automata learning on this system. I have downloaded the learnlib bundled binaries and the whole learnlib project from github. Using command prompt without Maven, I was able to run the example of using L* on the original unknown DFA in Angluin's 1987 paper, ie the DFA which accepts an even number of a's and b's. 

I have searched for a guide on how to set up basic active learning with learnlib on real systems without success. The best resource I found is http://ls5-www.cs.tu-dortmund.de/projects/learnlib/learnlib-tutorial.php - It appears to be an API tutorial which covers the setting of a test driver. 

Please let me know if there is a good resource that I can follow - it should cover the communications between the test driver and the SUL. My idea is as follows:

1. Model the lift as a Mealy machine, set the maximum number of states to, say 4. 

2. The learner is a Java console program which uses the learnlib JAR binary

3. Set up a test driver (which learnlib library?) which receives input symbol sequences from the learner and transforms it into a test case to the SUL

4. Test driver will read replies from the SUL and transform them into output symbol and relay it to the learner.

5. Reset the SUL for the next query.

Best Regards

Teck Ping

[Markus Frohme]

Hi Teck Ping,


oh dear, you dug out quite the fossil. Unfortunately, this page is about
an older version of LearnLib (named JLearn) which is out of date and no
longer maintained. I made sure to add a disclaimer to prevent confusion in
the future.

The best resources for the current LearnLib are probably the Github wiki
or the in-tree examples project [0]. If you look at the basic learning
setup, the parts that are always application-specific are the alphabet
definition and the MembershipOracle implementation, so these are the
things you would have to implement for your PLC lift. Since you want to
infer a Mealy Machine, you can also get a little bit more low-level and
provide an implementation of the SUL interface directly -- this usually
makes it easier map the reactive input/output behavior of the system. The
SUL can later be wrapped in a "SULOracle" to plug it into a
learner/equivalence oracle.

For the SUL you have to provide implementations for the #pre, #step and
#post methods. In your scenario it would make sense to

* in the pre method: initialize the TCP connection and set the lift to its
initial position (i.e. reset it).

* in the step method: sent your defined input actions (e.g. move up, move
down) over the TCP connection and return the responses (e.g. moved up,
moved down, reached maximum level, reached minimum level)

* in the post method: close the TCP connection and cleanup up any other
resources.

You could then plug it all together (i.e. which learning algorithm to use,
which equivalence oracle to use, etc.) and build a standalone executable
JAR which you can then run from the command line.

I can also look into adding a specific example to the LearnLib repository
that involves such a learning setup with a custom SUL, since the current
examples indeed do not cover this case.


Kind regards,
Markus


[0] - https://github.com/LearnLib/learnlib/tree/learnlib-0.14.0/examples

[Teck Ping Khoo]

Hi Markus

Thanks for your detailed answer. Following your hints, and with examples such as Turtlebot and TeaMachine, I was able to use Eclipse with Maven to learn a simple Mealy machine. 

I have a further question. In my use case, triggering one input to the lift can result in a series of outputs over time. For example, if the lift is now at level 1 and the input is the pressing of the level 2 button, the output will be the following events:

Lift move up (rising edge)

Lift move up (falling edge)

Door open

Door close

Does Learnlib support the learning of automata where a single input can lead to multiple outputs? Or should I stick to using a Mealy machine and encode these four outputs as a single output (meaning it becomes a single symbol in the output alphabet)?

Thanks!

Teck Ping

[Markus Frohme]

Dear Teck Ping,


currently, LearnLib (and AutomataLib) does not support non-output-deterministic automata (such as MealyMachines with epsilon transitions, which after parsing "Level 2" some time later could output "Door open" or "Door closed").

However, you are not restricted to simple types in your output alphabet. Instead of a MealyMachine<?, I, ?, O> you could also implement a MealyMachine<?, I, ?, Word<O>> (or SUL<I, Word<O>> for that matter). Technically, that is an encoding of your outputs, but one that still preserves the structural information of the output compared to, say, transforming everything into a String.

The only potential drawback is, that your inferred MealyMachine now computes Word<Word<O>> as outputs. So you would probably have to flatten the result, if you are interested in the plain sequence of outputs, that your lift returned.


Kind regards,
Markus

> --
> You received this message because you are subscribed to the Google Groups "LearnLib Q&A" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to learnlib-qa...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/learnlib-qa/95bcf141-81ea-4aa8-b610-754d1b9cbf48%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Teck Ping Khoo]

Hi Markus

Thanks for your reply. After some pondering, I realized that my use case is more specific - Allow me to explain:

The SUL is actually that of a bug, not the entire lift controller. When the lift has just closed its doors, if the lift car floor button of the same floor is pressed within 1s, the door will open when the lift is moving (which is the bug). To explain further, it is normal for the lift door to open when the floor button (inside the lift) for the current floor is pressed, when the lift is not moving. However, when this same input is applied within 1s after the lift moves off, it becomes an abnormal behavior. 

The target model should therefore be a DFA which accepts strings that trigger the bug, and not a Mealy machine. Let the symbol "a" represent the floor 1 button pressed and the symbol "b" be the floor 2 button pressed. Let "a1" mean that "a" occurs after 0.5s, "a2" mean that "a" occurs after 1.0s, and so on, till "a10" (means "a" delayed for 5s). I can similarly define "b1" to "b10". This will make up an alphabet of 20 symbols "a1", "a2", ..."a10" and "b1", "b2", ... "b10". A string like a "b1", "a2", "b9" will trigger the bug. This means that we request the lift move to floor 2, en route we press floor 1, and within 1s when the lift door closes at floor 2 to move to floor 1, we press floor 2. 

I tried to find an example of using LearnLib to build a DFA using the "pre()","step()" and "post()" methods of the "TestSUL" interface but could not find any. Does "TestSUL" support the learning of a DFA? Does the output of "step()" only support feeding back the output of a Mealy Machine state, or does it also support feedback of the acceptance of a word by the target DFA?

If "step()" works for learning a DFA, I only require the input of "step()" (as below) to be a Word, right?

public Boolean step(Input a_input) throws SULException

Thanks!

Teck Ping

> To unsubscribe from this group and stop receiving emails from it, send an email to learn...@googlegroups.com.

[Teck Ping Khoo]

Hi Markus

My apologies, the interface name mentioned should be just "SUL" and not "TestSUL". 

Regards

Teck Ping

[Markus Frohme]

Hi Teck Ping,


the SUL interface is specifically for reactive systems which translate to MealyMachines. However, you can just jump one level higher and directly provide a (DFA)MembershipOracle implementation or a SingleQueryOracle(DFA) implementation, if you want a simpler interface and don't care about parallelization, e.g.:

DFAMembershipOracle<I> mqOracle = new SingleQueryOracleDFA<I>() {

@Override
public Boolean answerQuery(Word<I> prefix, Word<I> suffix) {
// open connection
Connection c = new Connection(...);

// send over TCP
Result r = c.send(prefix.concat(suffix));

// interpret results
return r.isGood();
}
};


A few remarks:

* You could also handle the connection outside of the oracle and simply reset the lift in the beginning, which may be faster. The above is just a straight adaption from the SUL structure.

* The prefix, suffix split means that after transitioning the system under learning to the state reached by "prefix", only the "suffix" should determine the output. This is mostly relevant for MealyMembershipOracles, where the length of outputs matter. Since you only care about the single boolean result, it is fine here, to simply concat the two values and regard them as a single input sequence.

* You already did a good job, encoding the timing constraints into different symbols, since there is currently no concept of timed automata. I don't know to which extend your lift supports these timing information, but if it is a real-time system, you may have to fiddle around a little bit with Thread.sleep(), etc.


Kind regards,
Markus

On Sun, Jul 14, 2019 at 09:42:48PM -0700, Teck Ping Khoo wrote:
> Hi Markus
>

> Thanks for your reply. After some pondering, I realized that my use case is
> more specific - Allow me to explain:
>

> The SUL is actually that of a *bug*, not the entire lift controller. When
> the lift has just closed its doors, if the lift car floor button of the *same
> *floor is pressed within 1s, the door will open when the lift is moving

> (which is the bug). To explain further, it is normal for the lift door to
> open when the floor button (inside the lift) for the current floor is
> pressed, when the lift is not moving. However, when this same input is
> applied within 1s after the lift moves off, it becomes an abnormal
> behavior.
>
> The target model should therefore be a DFA which accepts strings that
> trigger the bug, and not a Mealy machine. Let the symbol "a" represent the
> floor 1 button pressed and the symbol "b" be the floor 2 button pressed.
> Let "a1" mean that "a" occurs after 0.5s, "a2" mean that "a" occurs after
> 1.0s, and so on, till "a10" (means "a" delayed for 5s). I can similarly
> define "b1" to "b10". This will make up an alphabet of 20 symbols "a1",
> "a2", ..."a10" and "b1", "b2", ... "b10". A string like a "b1", "a2", "b9"
> will trigger the bug. This means that we request the lift move to floor 2,
> en route we press floor 1, and within 1s when the lift door closes at floor
> 2 to move to floor 1, we press floor 2.
>
> I tried to find an example of using LearnLib to build a DFA using the
> "pre()","step()" and "post()" methods of the "TestSUL" interface but could
> not find any. Does "TestSUL" support the learning of a DFA? Does the output
> of "step()" only support feeding back the output of a Mealy Machine state,
> or does it also support feedback of the acceptance of a word by the target
> DFA?
>
> If "step()" works for learning a DFA, I only require the input of "step()"
> (as below) to be a Word, right?
>
>

> *public Boolean step(Input a_input) throws SULException*

[Teck Ping Khoo]

Hi Markus

Thanks for the guidance and encouragement - I will continue exploring. 

As an intermediate step to my goal, I experimented with using TTT for learning a basic Mealy Machine and a basic DFA. 

The Mealy Machine's alphabet is {a,b} and it is an edge detector - it outputs True when the last two inputs are different. The DFA's alphabet is also {a,b} and it only accepts ab. 

Attached are the java files and an image each for the Mealy Machine and the DFA. The Mealy Machine works. However, when I tried to use a similar method to learn the DFA, no counterexamples were found. I suspect I may have implemented "processQueries()" in the java file for the DFA wrongly. Any guidance appreciated.

Best Regards

Teck Ping

[Teck Ping Khoo]

Hi Markus

By following your previous suggestion closely I was able to get the DFA learning to work. Instead of implementing DFAMembershipOracle I implemented SingleQueryOracleDFA and overwrote the answerQuery() method. The working java file is as attached. 

To recap, my original goal is to learn a fault model. I will now move on to develop the answerQuery() method to interface to my miniature lift. Whatever learning algorithm (eg DHC, TTT) will iterate through the needed combinations of symbols in the alphabet. When a bug occurs answerQuery() will return true, otherwise it will return false. 

I will provide any results here. 

Thanks Markus, for your guidance so far.

Regards

Teck Ping

[Markus Frohme]

Hi Teck Ping


in your first example you used strInputWord == "ab" to determine the answer. For non-primitive types, == compares the references of two objects in Java. Two strings - even if they contain the same characters - are not necessarily the same object, i.e. "abc" == "abc" may evaluate to false (depending on whether or not the JVM has already interned the two String objects). You should have used "ab".equals(strInputWord) instead to reliably compare the contents.

In your second example, you used our Word class (and its equals method) which correctly compares the contents of the word. However, the code only accepts "ab" and not every word where the last two symbols differ, like you initially intended. I would have probably written:


final Word<String> input = prefix.concat(suffix);
final int length = input.length();

return length > 1 && !Objects.equals(input.getSymbol(length - 1), input.getSymbol(length - 2));


Kind regards,
Markus

On Tue, Jul 16, 2019 at 08:56:24AM -0700, Teck Ping Khoo wrote:
> Hi Markus
>

[Teck Ping Khoo]

Hi Markus

Thanks so much for reviewing the code! 

For your first feedback, I will take note of it and update the code accordingly. 

For your second feedback, you may have misunderstood my examples. My Mealy Machine example will return true when the last two symbols are different. It uses a membership oracle that fully defines the state transition. Of course, I can modify this oracle to actually define the output to be true when the last two inputs are different, like your suggested code. My DFA example will accept only "ab". It uses a membership oracle that defines only the acceptance of the input word "ab". So, the code should be correct. 

:)

Regards

Teck Ping