🥮 mooncakes.io
    Sign in

    moon-statelens

    Active black-box Mealy model learning and replay-confirmed behavioral compatibility checks.

    automata-learning
    mealy
    model-inference
    testing
    Download zip
    Version
    0.1.0
    License
    Apache-2.0
    Repository
    Last updated
    7 days ago
    Downloads
    68

    #Tested embedding example

    Add CaptainK-65/moon-statelens@0.1.0 to your module and this import to its moon.pkg:

    ///|
    import {
      "CaptainK-65/moon-statelens" @lens,
    }

    The following blocks are executed by moon test. The learner sees only the adapter, not the hidden state or a supplied reference model. Its conclusion is conditional on the declared two-state bound and resettable deterministic Mealy assumptions.

    ///|
    test "quick start learns a resettable session" {
      let active = [false]
      let target = @lens.System::new(reset=() => active[0] = false, step=input => {
        match input {
          "login" => {
            active[0] = true
            "ok"
          }
          "logout" => {
            active[0] = false
            "ok"
          }
          "request" => if active[0] { "allowed" } else { "denied" }
          _ => raise @lens.UnknownInput(input)
        }
      })
      let experiment = @lens.Experiment::new(target, ["login", "logout", "request"])
      let result = @lens.learn(experiment, @lens.Oracle::w_method(2))
      assert_true(result.status is Supported(ConditionalStateBound(2)))
      let model = result.model.unwrap()
      assert_eq(model.state_count(), 2)
      assert_eq(model.trace(["login", "logout", "request"]), ["ok", "ok", "denied"])
      assert_true(
        @lens.distinguish(model, @lens.decode_model(model.encode())) is None,
      )
    }

    Budget exhaustion is data, not equivalence:

    ///|
    test "quick start preserves an inconclusive query budget" {
      let target = @lens.System::new(reset=() => (), step=_ => "ok")
      let experiment = @lens.Experiment::new(target, ["x"], max_queries=0)
      let result = @lens.learn(experiment, @lens.Oracle::w_method(1))
      assert_true(result.status is Inconclusive("physical-queries"))
      assert_true(result.model is None)
    }

    LensError

    source
    pub(all) suberror LensError {
      InvalidArgument(String)
      UnknownInput(String)
      LimitExceeded(String)
      InconsistentObservation(word~ : Array[String], expected~ : Array[String], actual~ : Array[String])
    } derive(
    Debug    )

    Invalid inputs, inconsistent observations and explicit resource limits.

    LensError::to_repr

    source

    CheckResult

    source
    pub(all) enum CheckResult {
      Counterexample(Array[String])
      NoCounterexample(Evidence)
      Inconclusive(String)
    } derive(
    Debug    )

    Custom oracle contract: returned counterexamples must actually distinguish the supplied hypothesis from the experiment's target.

    CheckResult::to_repr

    source

    CompatibilityResult

    source
    pub(all) struct CompatibilityResult {
      status : CompatibilityStatus
      left : LearningResult
      right : LearningResult
      left_statistics : Statistics
      right_statistics : Statistics
      refinements : Int
      spurious_inputs : Array[Array[String]]
    } derive(
    Debug    )

    CompatibilityResult::to_json

    source

    CompatibilityResult::to_repr

    source

    CompatibilityStatus

    source
    pub(all) enum CompatibilityStatus {
      ConfirmedDifference(Difference)
      NoDifferenceBetweenHypotheses
      Inconclusive(String)
      ReplayUnstable(side~ : String, word~ : Array[String], expected~ : Array[String], actual~ : Array[String])
    } derive(
    Debug    )

    CompatibilityStatus::to_json

    source

    CompatibilityStatus::to_repr

    source

    Difference

    source
    pub(all) struct Difference {
      inputs : Array[String]
      left_outputs : Array[String]
      right_outputs : Array[String]
    } derive(Eq, ToJson, 
    Debug    )

    A replayable difference between two complete models.

    Difference::equal

    source
    fn Difference::equal(Difference, Difference) -> Bool

    Difference::not_equal

    source
    fn Difference::not_equal(x : Difference, y : Difference) -> Bool

    Difference::to_json

    source
    fn Difference::to_json(Difference) -> Json

    Difference::to_repr

    source

    Evidence

    source
    pub(all) enum Evidence {
      ExactReference
      ConditionalStateBound(Int)
      Budgeted(String)
    } derive(
    Debug    )

    Scope of the experiment that supported a hypothesis. ExactReference refers to a supplied explicit reference model; it does not certify an arbitrary adapter.
    impl ToJson for Evidence

    Evidence::to_json

    source
    fn Evidence::to_json(self : Evidence) -> Json

    Evidence::to_repr

    source

    Experiment

    source
    pub struct Experiment {
      // private fields
    }

    Bounded experiment session, with a prefix trace cache and consistency checks. Do not run a session concurrently or mutate a target outside its adapter.

    Experiment::alphabet

    source
    fn Experiment::alphabet(self : Experiment) -> Array[String]

    Experiment::new

    source
    fn Experiment::new(system : System, alphabet : Array[String], max_queries? : Int, max_steps? : Int, max_word_length? : Int, max_cache_nodes? : Int, max_output_code_units? : Int, use_cache? : Bool, recheck_every? : Int) -> Experiment raise LensError

    Experiment::query

    source
    fn Experiment::query(self : Experiment, requested_word : Array[String], bypass_cache? : Bool) -> Array[String] raise

    Query one word. Every physical execution starts with reset and ends with close. Bypass forces a new observation, checked against every previously observed prefix.

    Experiment::statistics

    source
    fn Experiment::statistics(self : Experiment) -> Statistics

    LearningResult

    source
    pub(all) struct LearningResult {
      model : Machine?
      status : LearningStatus
      statistics : Statistics
      rounds : Array[LearningRound]
      counterexamples : Array[Difference]
    } derive(
    Debug    )

    LearningResult::to_json

    source
    fn LearningResult::to_json(self : LearningResult) -> Json

    LearningResult::to_repr

    source

    LearningRound

    source
    pub(all) struct LearningRound {
      index : Int
      states : Int
      prefixes : Int
      suffixes : Int
      table_cells : Int
      table_symbols : Int
      queries : Int
      counterexample_length : Int?
    } derive(ToJson, 
    Debug    )

    LearningRound::to_json

    source

    LearningRound::to_repr

    source

    LearningStatus

    source
    pub(all) enum LearningStatus {
      Supported(Evidence)
      Inconclusive(String)
      Unstable(word~ : Array[String], expected~ : Array[String], actual~ : Array[String])
    } derive(
    Debug    )

    LearningStatus::to_json

    source
    fn LearningStatus::to_json(self : LearningStatus) -> Json

    LearningStatus::to_repr

    source

    Machine

    source
    pub struct Machine {
      // private fields
    } derive(
    Debug    )

    Validated model; construction and accessors defensively copy arrays.
    impl ToJson for Machine

    Machine::access_sequences

    source
    fn Machine::access_sequences(self : Machine) -> Array[(Int, Array[String])]

    Shortest access words for reachable states, in BFS/input order.

    Machine::alphabet

    source
    fn Machine::alphabet(self : Machine) -> Array[String]

    Machine::characterizing_set

    source
    fn Machine::characterizing_set(self : Machine, max_work? : Int) -> Array[Array[String]] raise LensError

    Pairwise shortest distinguishing suffixes for a reachable minimal model. Includes epsilon so single-state models test outputs. Preparation and witness reconstruction share a work budget; exhaustion never returns a partial set.

    Machine::distinguish_states

    source
    fn Machine::distinguish_states(self : Machine, left : Int, right : Int) -> Array[String]? raise LensError

    Distinguish two states of one model. Equivalent states return None.

    Machine::encode

    source
    fn Machine::encode(self : Machine) -> String

    Encode a model in the versioned interchange format.

    Machine::from_json

    source
    fn Machine::from_json(value : Json) -> Machine raise

    Decode a versioned complete model, then apply all constructor invariants.

    Machine::initial_state

    source
    fn Machine::initial_state(self : Machine) -> Int

    Machine::minimize

    source
    fn Machine::minimize(self : Machine, max_work? : Int) -> Machine raise LensError

    Remove unreachable states and merge observationally equivalent states. The result uses BFS numbering starting at state zero.

    Machine::new

    source
    fn Machine::new(alphabet : Array[String], transitions : Array[Array[Transition]], initial? : Int) -> Machine raise LensError

    Construct a complete machine. Table columns follow alphabet order.

    Machine::state_count

    source
    fn Machine::state_count(self : Machine) -> Int

    Machine::system

    source
    fn Machine::system(self : Machine) -> System

    Treat this explicit model as a black box. The learner receives only callbacks.

    Machine::table

    source
    fn Machine::table(self : Machine) -> Array[Array[Transition]]

    Machine::to_dot

    source
    fn Machine::to_dot(self : Machine) -> String

    DOT uses quoted JSON string escapes for textual labels, so quotes, backslashes and line breaks cannot escape into graph statements.

    Machine::to_json

    source
    fn Machine::to_json(self : Machine) -> Json

    Machine::to_repr

    source

    Machine::trace

    source
    fn Machine::trace(self : Machine, word : Array[String]) -> Array[String] raise LensError

    Execute an input word starting at the model's initial state.

    Machine::trace_from

    source
    fn Machine::trace_from(self : Machine, state : Int, word : Array[String]) -> Array[String] raise LensError

    Execute an input word starting at an explicitly selected state.

    Oracle

    source
    pub struct Oracle {
      // private fields
    }

    Oracle::evaluate

    source
    fn Oracle::evaluate(self : Oracle, hypothesis : Machine, experiment : Experiment) -> CheckResult raise

    Run a conformance oracle directly. Unlike learn, this propagates resource limits to the caller. Hypothesis and experiment alphabets must agree.

    Oracle::exact

    source
    fn Oracle::exact(reference : Machine, max_pairs? : Int) -> Oracle raise LensError

    Exact equivalence to a supplied explicit model. Intended for fixtures and independent algorithm tests. The caller must establish that the adapter implements that reference; this oracle cannot establish it for an unknown SUL.

    Oracle::exhaustive

    source
    fn Oracle::exhaustive(max_depth : Int, max_tests? : Int) -> Oracle raise LensError

    Fresh exhaustive experiments through max_depth. Completion is bounded evidence only. max_tests or an experiment limit yields Inconclusive.

    Oracle::new

    source
    fn Oracle::new(check : (Machine, Experiment) -> CheckResult raise) -> Oracle

    Oracle::random_words

    source
    fn Oracle::random_words(seed? : UInt, max_length? : Int, tests? : Int) -> Oracle raise LensError

    Reproducible random-word experiments. Successful completion is never an unconditional equivalence result. The seed is reset for each hypothesis.

    Oracle::w_method

    source
    fn Oracle::w_method(state_bound : Int, max_tests? : Int, max_characterization_work? : Int) -> Oracle raise LensError

    Complete W-method suite P . Sigma^{<=m-n} . W, where P is a transition cover and W characterizes a minimized, reachable hypothesis. Completeness is conditional on the actual SUL satisfying the declared state bound and deterministic, total, resettable Mealy assumptions. Truncation is inconclusive.

    Oracle::with_regressions

    source
    fn Oracle::with_regressions(self : Oracle, words : Array[Array[String]]) -> Oracle

    Replay supplied regression words before delegating to this oracle. Words are copied; observations bypass the cache and can refine a stale hypothesis.

    Statistics

    source
    pub(all) struct Statistics {
      queries : Int
      cache_hits : Int
      resets : Int
      steps : Int
      completed_queries : Int
      cache_nodes : Int
      output_code_units : Int
    } derive(ToJson, 
    Debug    )

    Immutable counters. Queries count logical requests; resets and steps count attempted target calls, including failed calls. Cache hits execute no target code.

    Statistics::to_json

    source
    fn Statistics::to_json(Statistics) -> Json

    Statistics::to_repr

    source

    System

    source
    pub struct System {
      // private fields
    }

    Reset/step adapter. Callbacks may raise; close is attempted on every physical query.

    System::new

    source
    fn System::new(reset~ : () -> Unit raise, step~ : (String) -> String raise, close? : () -> Unit raise) -> System

    Transition

    source
    pub(all) struct Transition {
      target : Int
      output : String
    } derive(Eq, ToJson, 
    Debug    , 
    FromJson    )

    One transition of a complete deterministic Mealy machine.

    Transition::equal

    source
    fn Transition::equal(Transition, Transition) -> Bool

    Transition::from_json

    source

    Transition::not_equal

    source
    fn Transition::not_equal(x : Transition, y : Transition) -> Bool

    Transition::to_json

    source
    fn Transition::to_json(Transition) -> Json

    Transition::to_repr

    source

    compare

    source
    fn compare(left : Experiment, right : Experiment, left_oracle : Oracle, right_oracle : Oracle, max_states? : Int, max_refinements? : Int) -> CompatibilityResult raise

    Infer both behaviors and replay model differences on the real adapters. Spurious hypothesis disagreements refine later experiments. Equal hypotheses remain qualified by each learning result's evidence. Final statistics include the real confirmation calls, even when those calls exhaust a budget.

    confirm_difference

    source
    fn confirm_difference(left : Experiment, right : Experiment, inputs : Array[String]) -> Difference? raise

    Freshly replay a candidate word against both real targets. None means the candidate did not reproduce a difference.

    decode_model

    source
    fn decode_model(text : String, max_code_units? : Int) -> Machine raise

    Parse a bounded JSON document (limit counts UTF-16 code units, not bytes).

    distinguish

    source
    fn distinguish(left : Machine, right : Machine, max_pairs? : Int) -> Difference? raise LensError

    BFS in the reachable product graph. None is exact observable equivalence of the two supplied complete models, not a theorem about unknown programs.

    learn

    source
    fn learn(experiment : Experiment, oracle : Oracle, max_states? : Int, max_rounds? : Int, max_table_cells? : Int, max_table_symbols? : Int, max_prefixes? : Int) -> LearningResult raise

    Learn only through experiment queries. The oracle searches for counterexamples; its evidence determines what a Supported status actually means. Resource limits return Inconclusive with the last completed hypothesis, if any.

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io