Learning Based Testing with AALpy

Learning-based testing can be set up in 2 distinct ways:

• we learn two or more systems and then cross-check their models for cases of non-conformance
• we learn a single system and use its model as a hypothesis for the other systems

Let us demonstrate how to set up the second case.

If you would like to learn several systems that should conform to the same specification, a reasonable assumption is that you can reuse SUL implementation for all systems. Note that this assumption is not necessary, but for brevity, we will assume it.

imports ...
# MqttSUL implements the SUL interface for the Mqtt Client
# client that we are going to learn
mqtt_impl_1 = MqttSUL(client1)

# client(s) that we are going to test
mqtt_impl2 = MqttSUL(client2)
...

alphabet = client1.get_input_alphabet()

eq_oracle = RandomWalkEqOracle(alphabet, mqtt_impl_1,num_steps = 5000,reset_after_cex=True)

learned_model = run_Lstar(alphabet, sul, eq_oracle)

# at this point, model is learned
# to do the Learning-based testing, we simply use the model as a hypothesis for other systems/implementations
# in cases of non-conformance, counterexample will be returned

# note that the SUL passed to the eq_oracle is not the one that we used for learning
eq_oracle = RandomWalkEqOracle(alphabet, mqtt_impl_2, num_steps=5000,reset_after_cex=True)

counter_example = eq_oracle.find_cex(learned_model)
if counter_example:
  print('Counterexample found', counter_example)
else:
  print('No counterexample found')