Learning Based Testing with AALpy

Learning-based testing setup

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, 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.

# 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 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')