Add black-box checking and runtime monitoring

[bpellen]

Add support for black-box checking and runtime monitoring.

[emuskardin]

Due to lack of time, I did initial detailed review with Claude, went through it, and picked up from it most important points. These should all be easy to address, and once addressed, I will look at it again.

Also please add a minimal example at the bottom of Examples.py for the functionality that you have added.

---

1. Blocker — missing annotation imports break the library on Python < 3.14

Nine names are used in type annotations without being imported.
NameError: name 'Callable' is not defined. Did you mean: 'callable'?

1.1 Why this passed locally

Python 3.14 implements PEP 649: annotations are evaluated lazily. Before 3.14 they are evaluated eagerly at def time, i.e. at import. Same

from typing import Any          # Callable is NOT imported
def f(tag: Callable[[Any], Any], xs: List[str] | None = None): ...

• Python 3.11 — import aalpy raises NameError; the 86 new tests cannot even be collected.
• Python 3.14 — import aalpy succeeds; all 86 new tests pass.

All nine undefined names sit in annotation position, which is exactly why the suite looked green. pyproject.toml declares requires-python on four of the five supported versions.

Exact fix, per file

1. aalpy/utils/HelperFunctions.py — missing Callable, List. Line 6: change from typing import Any to from typing import Any, Callable, List.
2. aalpy/utils/HelperFunctions.py — missing MealyMachine. Line 8: add MealyMachine to from aalpy import Mdp, MarkovChain, McState, MooreMa
3. aalpy/model_checking_oracles/IUOBugDfaModelCheckingOracle.py — missing Any. Change from typing import Callable, List, Tuple to from typing import Any, Callable, List, Tuple.
4. tests/SULs/test_monitoring_sul.py — missing Tuple. Line 1: change from typing import Any to from typing import Any, Tuple.
5. tests/model_checking_oracles/test_iuo_bug_dfa_model_checking_oracle.py — missing Any, Tuple. Add from typing import Any, Tuple.
6. tests/oracles/test_bbc_eq_oracle.py — missing Any, Tuple, Automaton, InputType. Add from typing import Any, Tuple and from aalpy.base.AputType.
7. tests/property_monitors/test_iuo_bug_dfa_monitor.py — missing Any, Tuple. Add from typing import Any, Tuple.
8. tests/utils/test_helper_functions.py — missing Any, Tuple. Add from typing import Any, Tuple.
9. tests/model_checking_oracles/test_iuo_bug_dfa_model_checking_oracle.py:288 — genuine typo, unrelated to imports: Mealy should be MealyMachine.

On item 6: InputType is not re-exported from aalpy.base. It must come from aalpy.base.Automaton, the same way aalpy/base/Oracle.py imports it.

---

2. Bugs and logical inconsistencies

2.1 IUOBugDfaModelCheckingOracle.find_cex hangs forever on cyclic models

IUOBugDfaModelCheckingOracle.py:99-101 writes BFS parent pointers unconditionally, before the if next_pair not in explored guard:

parents[next_pair] = current_pair
letters_to_parents[next_pair] = letter

When the product BFS revisits an already-explored pair — including the initial pair — this overwrites that node's parent. Overwriting lettir] destroys the None sentinel that witness reconstruction relies on:

while p is not None:
    sym = letters_to_parents[p]
    if sym is None: break       # never reached once the sentinel is clobbered
    word = [sym] + word

The parent chain becomes cyclic and the loop spins forever while word grows unbounded.

• Repro (confirmed, killed at 15s; expected ('b',)): Mealy q0 -a/x-> q0, q0 -b/y-> q1; bug DFA b0 -a-> b1 -x-> b0 (back to init) plus b0 -b-> b2 -y-> b3 accepting.
• Severity: needs only a self-loop in the hypothesis — nearly every learned model has one.
• Fix: move both assignments, and the accepting check, inside the not in explored guard.

2.2 MonitoringSUL.query crashes on the empty word — DFA/Moore learning unusable

MonitoringSUL.py:183:

if len(word) == 0:
    self.steps += 1          # no such attribute — should be self.num_steps
                                                                                                                                                                                                                                                                                                                  AttributeError: 'MonitoringSUL' object has no attribute 'steps'. Did you mean: 'step'?

                                                                                                                                                                                                                                                                                                              L* queries ε in the first round for DFAs, so run_Lstar over a DFA with a MonitoringSUL dies immediately. Uncaught because no new test covedd one.
                                                                                                                                                                                                                                                                                                               **Violation callback receives a live, mutating list**

MonitoringSUL.step passes self.inputs by reference; it keeps growing for the rest of the query. A callback that stores its argument — the obvious use — gets the whole query word, not the counterexample prefix:

captured at callback time should be ['a','b'] -> actually: ['a','b','a','a']

This silently corrupts every counterexample the feature exists to deliver. Pass tuple(self.inputs); BBCEqOracle should match.
Dead statement in BBCEqOracle.find_cex → inconsistent return type

if cex is not None:
    tuple(cex)        # result discarded — no-op

Property counterexamples return as lists while the eq_oracle path returns tuples (cex = tuple(cex)). The base contract is tuple[InputType, ...] | None, and downstream cex processing hashes/indexes these. Also collapse the redundant double if cex is not None:.
Silent state-ID collisions in IUO_dfa_from_IXO_dfa
Auxiliary states are keyed by a synthesized ID f"O{o}D{dst}" looked up in the same iuo_state_map holding the original states. An original state whose ID matches a synthesized one is silently reused, corrupting the product. Same risk for the hardcoded "sink_state". Add a uniqueness assertion or a separate map.

Minor stuff

• inputs/outputs are built from get_input_alphabet() without dedup, so each holds one entry per (i,o) pair; loops re-run |O| times per input.
• dfa.get_input_alphabet() recomputed inside the nested input-completion loop.
• IUOBugDfaModelCheckingOracle.find_cex never increments num_queries/num_steps, so a wrapping BBCEqOracle reports nothing; reset_hyp_and_sul is effectively dead code.
• Unused from aalpy.base.SUL import SUL in the model-checking oracle.

---

Design Stuff

1. PropertyMonitor is in the wrong package. The ABC lives in aalpy/SULs/MonitoringSUL.py while implementations live in aalpy/property_monitors/. AALpy puts every abstract base in aalpy/base/ (Automaton, SUL, Oracle) — PropertyMonitor belongs there.

2. Copy-pasted base-class methods. MonitoringSUL duplicates SUL.query/adaptive_query rather than delegating. Two consequences: (i) it has already drifted — the copies carry the old Google Args:/Returns: docstrings while aalpy/base/SUL.py migrated to reST :param:, and that stale snapshot is how the self.steps bug got in; (ii) it bypasses the wrapped SUL's own query, so wrapping a CacheSUL silently disables caching, since only self.sul.step() is ever called.
   Fit with AALpy's design logic and language

3. No attribute forwarding. CacheSUL gained getattr forwarding two commits ago (ca24a8a, 6813d0a) precisely so wrappers stay transparent. MonitoringSUL is a new wrapper that should follow the pattern the repo just established.

4. Bare string literals used as comments throughout MonitoringSUL and BBCEqOracle — e.g. a """Bind the number of queries…""" block placed above @Property. These are no-op expressions, not docstrings. AALpy uses # here. The two above query/adaptive_query are worse: they precede the def, so each method then has a second, real docstring.

5. Constructor side effects on wrapped objects. Both wrappers call super().init(...) after binding the wrapped object, which routes through the delegating property setters. Constructing a BBCEqOracle silently overwrites the wrapped oracle's alphabet and sul and zeroes its counters; MonitoringSUL likewise resets the wrapped SUL's counters. Document it, or assert the alphabets agree instead of clobbering.

6. Export inconsistency. aalpy/init.py promotes BBCEqOracle, IUOBugDfaModelCheckingOracle and IUOBugDfaMonitor, but not MonitoringSUL or PropertyMonitor, so users cannot write a custom monitor from the top-level import. Promote all five or none.

[bpellen]

I added two Oracle-specific counters to the IUOBugDfaModelCheckingOracle: one for the number of checks performed and one for the number of counterexamples that were found when performing these checks. It still uses the Oracle interface.

I also added randomly-generated exhaustive and non-exhaustive tests for both black-box checking and runtime monitoring, which I based on the instance you pointed me to (https://github.com/DES-Lab/AALpy/blob/master/tests/learning_algs/deterministic/test_random_learning_runs_exhaustive.py). The exhaustive tests only run with pytest --exhaustive, as expected. While working on the exhaustive BBC tests, I found that 5 of the 2400 tests crashed on line 240 (assert self.initial_state is not None) of aalpy/learning_algs/deterministic/ClassificationTree.py. This function reproduces the first of these 5 tests and crashes on that same line:

def reproduce():
    from aalpy.automata import MealyMachine
    from aalpy.base import Oracle, SUL
    from aalpy.learning_algs import run_KV
    from aalpy.SULs import AutomatonSUL

    mealy = MealyMachine.from_state_setup({
        's1': {'I0': ('O0', 's2'), 'I1': ('O1', 's3')},
        's2': {'I0': ('O2', 's1'), 'I1': ('O2', 's3')},
        's3': {'I0': ('O1', 's3'), 'I1': ('O2', 's1')},
    })
    sul = AutomatonSUL(mealy)

    counterexample = ('I0', 'I0', 'I1')

    class ExampleOracle(Oracle):
        def __init__(self, alphabet: list, sul: SUL):
            super().__init__(alphabet, sul)
        def find_cex(self, hypothesis: Automaton):
            # This hard-coded counterexample is valid for the initial hypothesis, which is the hypothesis for which the crash occurs
            assert self.sul.query(counterexample) != hypothesis.execute_sequence(hypothesis.initial_state, counterexample) 

            return counterexample
    eq_oracle = ExampleOracle(mealy.get_input_alphabet(), sul)

    run_KV(mealy.get_input_alphabet(), sul, eq_oracle, automaton_type="mealy", print_level=3)

All 5 of my failing tests pass when I ensure that the model checker counterexamples returned by the BBCEqOracle for hypothesis refinement are minimal (by taking their shortest prefixes that lead to distinct outputs between the hypothesis and the SUL). I changed the BBCEqOracle to always return these minimal prefixes (for model checker counterexamples, because these counterexamples are found between the property and the hypothesis and there is no particular reason to assume that they are minimal with respect to the hypothesis and the SUL). My tests now pass, but I wanted to inform you about these crashes because their root cause (in the ClassificationTree) still persists.

I fixed the faulty docstring you found in aalpy/property_monitors/IUOBugDfaMonitor.py, and I solved the de-duplication errors you found in IUO_dfa_from_IXO_dfa.

[emuskardin]

@bpellen , thanks, I will do (hopefully) a final check this workweek.

[emuskardin]

Python 3.14 on your machine again breaking stuff :p

Would recommend creating 3.11 or 3.12 venv

  tests/SULs/test_random_runtime_monitoring_runs.py:48: undefined name 'Any'
  tests/SULs/test_random_runtime_monitoring_runs.py:48: undefined name 'Tuple'
  tests/SULs/test_random_runtime_monitoring_runs_exhaustive.py:62: undefined name 'Any'
  tests/oracles/test_random_bbc_runs.py:48: undefined name 'Any'
  tests/oracles/test_random_bbc_runs_exhaustive.py:62: undefined name 'Any

# Take the minimal distinguishing prefix of the counterexample

for i in range(min(len(hyp_out), len(sul_out))):
    if hyp_out[i] != sul_out[i]:
        prop_cex = prop_cex[:i + 1]
        break

if not self.check_all_props_when_a_first_prop_cex_was_found:
    return cex        # <-- returns the UNTRUNCATED cex

The truncation writes to prop_cex, but the early return hands back cex. So with check_all_props_when_a_first_prop_cex_was_found=False the work is computed and thrown away:

check_all=True  -> returned cex ('a',)
check_all=False -> returned cex ('a', 'a', 'a')

Same shape as the tuple(cex) no-op from round 1 — value computed, wrong variable returned. Fix is return prop_cex.

Why it slipped through: check_all_props_when_a_first_prop_cex_was_found=False is set by no test in the repo — I grepped all of tests/. The whole flag is untested, including the 4800-case exhaustive sweep. A single parametrisation over (True, False) on an existing BBC test would cover it.

Missing assertion, tests/SULs/test_monitoring_sul.py:499-500 — expected_second_word_outputs is built but never compared, and the query result is assigned to first_word_outputs (copy-paste from line 483), shadowing the earlier value:
expected_second_word_outputs = ('o', 'o', 'o', 'x', 'o', 'o')
first_word_outputs = sul.query(second_word) # never asserted

Unused imports: MealyMachine, MealyState, generate_random_dfa, bisimilar in tests/property_monitors/test_iuo_bug_dfa_monitor.py; BBCEqOracle and generate_random_deterministic_automata in Examples.py (1481, 1484, 1387).

Examples.py — runtime_monitoring_example still prints "BBC confirmed counterexample…" though it performs no black-box checking

[emuskardin]

Regarding the bug you pointed out, that is not really a bug per se, as it would never happen in classic AL with oracles that return cex at the first occurring differance.

I will keep it in mind.

Is that something that your approach has? That the cex is non-minimal, that is, it is not trimmed to the first difference?

If yes, I would suggest fixing that if possible, much more elegant if cex shows the difference clearly. Also, some are of the opinion that if you cex is a sequance of inputs, the output of it is just the last output, which would make the cex not a cex if some middle input shows the differance. I do not subscribe to that school of thought, but some do.

So please check BBC oracle line 104 if I remember correctly, where you call SUL query to rather step the sul, and reset with pre and post appropriately.

You will save some queries, and be consistent with other oracles.

[bpellen]

@emuskardin, thank you for the additional feedback. I addressed your five points by:

Adding the missing imports. I now perform all of my testing from a Docker container that has Python 3.11 installed. I re-ran all of my unit tests and Examples, and I added every import that was revealed to be missing by the resulting crashes.

As requested, the BBCEqOracle now runs the property counterexamples as if they were test cases in any other equivalence oracle, using the reset_hyp_and_sul method, the hypothesis and SUL step methods, and the SUL's post method. Counterexample processing stops as soon as the hypothesis and SUL disagree on the output.
I changed my unit tests for the BBCEqOracle to explicitly test that the property counterexamples are truncated properly, both when self.check_all_props_when_a_first_prop_cex_was_found is True, and when it is False. Some unit tests also check that the num_queries and num_steps are updated properly in this new code.

I added the missing assertions to tests/SULs/test_monitoring_sul.py, and the outputs for the second word are no longer erroneously assigned to first_word_outputs.

I removed the unused imports that you mentioned.

I corrected the print statement to "Runtime monitoring confirmed counterexample...".

Cleanup.
I also resolved some inconsistencies in the notation that I used, regarding things such as the use of single vs. double quotes.