🥮 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.2.0
    License
    Apache-2.0
    Repository
    Last updated
    3 days ago
    Downloads
    67

    #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

    Algorithm

    source
    pub(all) enum Algorithm {
      LStar
      KearnsVazirani
    } derive(Eq, 
    Debug    )

    Structurally different Mealy learners sharing query and model infrastructure.

    Algorithm::equal

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

    Algorithm::name

    source
    fn Algorithm::name(self : Algorithm) -> String

    Algorithm::not_equal

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

    Algorithm::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

    DriverMetrics

    source
    pub(all) struct DriverMetrics {
      states : Int
      access_sequences : Int
      discriminators : Int
      table_cells : Int
      table_symbols : Int
      tree_nodes : Int
    } derive(ToJson, 
    Debug    )

    DriverMetrics::to_json

    source

    DriverMetrics::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
    }

    Synchronous compatibility facade over the IO-independent query session.

    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

    Experiment::statistics

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

    LearningDriver

    source
    pub struct LearningDriver {
      // private fields
    }

    IO-independent suspended learner. Execute Query using a QuerySession/runner; verify each Hypothesis, then refine with a freshly executed counterexample.

    LearningDriver::algorithm

    source
    fn LearningDriver::algorithm(self : LearningDriver) -> Algorithm

    LearningDriver::event

    source
    fn LearningDriver::event(self : LearningDriver, queries? : Int) -> LearningEvent raise LensError

    Repeated calls return the same outstanding event with defensive word copies.

    LearningDriver::metrics

    source

    LearningDriver::new

    source
    fn LearningDriver::new(algorithm : Algorithm, alphabet : Array[String], max_states? : Int, max_rounds? : Int, max_table_cells? : Int, max_table_symbols? : Int, max_prefixes? : Int) -> LearningDriver raise

    LearningDriver::refine

    source
    fn LearningDriver::refine(self : LearningDriver, requested : Array[String], actual : Array[String]) -> Unit raise

    Validate and trim a real counterexample at its first mismatching output.

    LearningDriver::result

    source
    fn LearningDriver::result(self : LearningDriver, statistics : Statistics, status : LearningStatus) -> LearningResult

    Snapshot the last COMPLETE hypothesis, never an in-progress transition table.

    LearningDriver::submit

    source
    fn LearningDriver::submit(self : LearningDriver, id : Int, outputs : Array[String]) -> Unit raise

    LearningEvent

    source
    pub(all) enum LearningEvent {
      Query(QueryRequest)
      Hypothesis(Machine)
    } derive(
    Debug    )

    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::plan

    source
    fn Oracle::plan(plan : VerificationPlan) -> Oracle raise LensError

    A synchronous facade over the same suspendable verification used by async IO.

    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.

    Oracle::wp_method

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

    QueryRequest

    source
    pub(all) struct QueryRequest {
      id : Int
      inputs : Array[String]
    } derive(
    Debug    )

    A requested physical query. The runner must reset, execute each input, then clean up successfully before committing. Arrays are defensive copies.

    QueryRequest::to_repr

    source

    QuerySession

    source
    pub struct QuerySession {
      // private fields
    }

    IO-independent cache, budgets and observation consistency. Exactly one outstanding query is allowed. Failed/cancelled work must be aborted.

    QuerySession::abort

    source
    fn QuerySession::abort(self : QuerySession, id : Int) -> Unit

    Discard an unfinished query. Idempotent after commit/abort for safe defers. A different outstanding request cannot be aborted by an old identifier.

    QuerySession::accept_output

    source
    fn QuerySession::accept_output(self : QuerySession, id : Int, output : String) -> Unit raise LensError

    QuerySession::alphabet

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

    QuerySession::commit

    source
    fn QuerySession::commit(self : QuerySession, id : Int) -> Array[String] raise LensError

    Commit only AFTER successful target cleanup. Conflicts poison the session.

    QuerySession::new

    source
    fn QuerySession::new(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) -> QuerySession raise LensError

    QuerySession::reset_started

    source
    fn QuerySession::reset_started(self : QuerySession, id : Int) -> Unit raise LensError

    Record the attempted reset immediately before invoking the target.

    QuerySession::start

    source
    fn QuerySession::start(self : QuerySession, requested : Array[String], bypass_cache? : Bool) -> QueryStart raise LensError

    QuerySession::statistics

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

    QuerySession::step_started

    source
    fn QuerySession::step_started(self : QuerySession, id : Int) -> Unit raise LensError

    Record an attempted step before invoking it, including attempts that fail.

    QueryStart

    source
    pub(all) enum QueryStart {
      Cached(Array[String])
      Execute(QueryRequest)
    } derive(
    Debug    )

    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. Attempts include target calls that fail.

    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

    VerificationCursor

    source
    pub struct VerificationCursor {
      // private fields
    }

    VerificationCursor::event

    source

    VerificationCursor::new

    source
    fn VerificationCursor::new(plan : VerificationPlan, hypothesis : Machine) -> VerificationCursor raise

    VerificationCursor::stages

    source

    VerificationCursor::submit

    source
    fn VerificationCursor::submit(self : VerificationCursor, id : Int, outputs : Array[String]) -> Unit raise

    VerificationEvent

    source
    pub(all) enum VerificationEvent {
      Query(QueryRequest)
      Completed(CheckResult)
    } derive(
    Debug    )

    VerificationPlan

    source
    pub(all) enum VerificationPlan {
      Exact(Machine)
      Exhaustive(depth~ : Int, max_tests~ : Int)
      RandomWords(seed~ : UInt, max_length~ : Int, tests~ : Int)
      WMethod(bound~ : Int, max_tests~ : Int, max_work~ : Int)
      WpMethod(bound~ : Int, max_tests~ : Int, max_work~ : Int)
      Replay(Array[Array[String]])
      Chain(Array[VerificationPlan])
    } derive(
    Debug    )

    Declarative, suspendable conformance strategies. State-bound methods require deterministic, total, reliably resettable targets and a CORRECT state bound.

    VerificationPlan::to_repr

    source

    VerificationStage

    source
    pub(all) struct VerificationStage {
      strategy : String
      tests : Int
      result : String
    } derive(ToJson, 
    Debug    )

    VerificationStage::to_json

    source

    VerificationStage::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.

    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

    Synchronous L* compatibility entry. The same suspended learner also powers native asynchronous runners.

    learn_with

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

    Select L* or KV without changing the synchronous custom-oracle contract.

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io