README
- ::to_reprLensError::to_repr
- ::equalAlgorithm::equal
- ::nameAlgorithm::name
- ::not_equalAlgorithm::not_equal
- ::to_reprAlgorithm::to_repr
- ::check_traceBehaviorRule::check_trace
- ::findingBehaviorRule::finding
- ::from_jsonBehaviorRule::from_json
- ::newBehaviorRule::new
- ::searchBehaviorRule::search
- ::to_jsonBehaviorRule::to_json
- ::verifyBehaviorRule::verify
- ::to_reprCheckResult::to_repr
- ::to_jsonCompatibilityResult::to_json
- ::to_reprCompatibilityResult::to_repr
- ::to_jsonCompatibilityStatus::to_json
- ::to_reprCompatibilityStatus::to_repr
- ::equalDifference::equal
- ::not_equalDifference::not_equal
- ::to_jsonDifference::to_json
- ::to_reprDifference::to_repr
- ::to_jsonDriverMetrics::to_json
- ::to_reprDriverMetrics::to_repr
- ::to_jsonEvidence::to_json
- ::to_reprEvidence::to_repr
- ::alphabetExperiment::alphabet
- ::newExperiment::new
- ::queryExperiment::query
- ::statisticsExperiment::statistics
- ::algorithmLearningDriver::algorithm
- ::eventLearningDriver::event
- ::metricsLearningDriver::metrics
- ::newLearningDriver::new
- ::refineLearningDriver::refine
- ::resultLearningDriver::result
- ::submitLearningDriver::submit
- ::to_reprLearningEvent::to_repr
- ::to_jsonLearningResult::to_json
- ::to_reprLearningResult::to_repr
- ::to_jsonLearningRound::to_json
- ::to_reprLearningRound::to_repr
- ::to_jsonLearningStatus::to_json
- ::to_reprLearningStatus::to_repr
- ::access_sequencesMachine::access_sequences
- ::alphabetMachine::alphabet
- ::characterizing_setMachine::characterizing_set
- ::distinguish_statesMachine::distinguish_states
- ::encodeMachine::encode
- ::from_jsonMachine::from_json
- ::initial_stateMachine::initial_state
- ::minimizeMachine::minimize
- ::newMachine::new
- ::regression_suiteMachine::regression_suite
- ::state_countMachine::state_count
- ::systemMachine::system
- ::tableMachine::table
- ::to_dotMachine::to_dot
- ::to_jsonMachine::to_json
- ::to_reprMachine::to_repr
- ::traceMachine::trace
- ::trace_fromMachine::trace_from
- ::to_jsonModelDiagnosis::to_json
- ::to_reprModelDiagnosis::to_repr
- ::evaluateOracle::evaluate
- ::exactOracle::exact
- ::exhaustiveOracle::exhaustive
- ::newOracle::new
- ::planOracle::plan
- ::random_wordsOracle::random_words
- ::w_methodOracle::w_method
- ::with_regressionsOracle::with_regressions
- ::wp_methodOracle::wp_method
- ::to_reprQueryRequest::to_repr
- ::abortQuerySession::abort
- ::accept_outputQuerySession::accept_output
- ::alphabetQuerySession::alphabet
- ::commitQuerySession::commit
- ::newQuerySession::new
- ::reset_startedQuerySession::reset_started
- ::startQuerySession::start
- ::statisticsQuerySession::statistics
- ::step_startedQuerySession::step_started
- ::to_reprQueryStart::to_repr
- ::equalRegressionCase::equal
- ::from_jsonRegressionCase::from_json
- ::not_equalRegressionCase::not_equal
- ::to_jsonRegressionCase::to_json
- ::to_reprRegressionCase::to_repr
- ::abortRegressionExecution::abort
- ::next_wordRegressionExecution::next_word
- ::observeRegressionExecution::observe
- ::reportRegressionExecution::report
- ::alphabetRegressionPlan::alphabet
- ::certificateRegressionPlan::certificate
- ::executionRegressionPlan::execution
- ::runRegressionPlan::run
- ::validateRegressionPlan::validate
- ::wordsRegressionPlan::words
- ::casesRegressionSuite::cases
- ::coverageRegressionSuite::coverage
- ::evidenceRegressionSuite::evidence
- ::from_jsonRegressionSuite::from_json
- ::is_completeRegressionSuite::is_complete
- ::planRegressionSuite::plan
- ::to_jsonRegressionSuite::to_json
- ::equalRuleEvent::equal
- ::from_jsonRuleEvent::from_json
- ::not_equalRuleEvent::not_equal
- ::to_jsonRuleEvent::to_json
- ::to_reprRuleEvent::to_repr
- ::to_jsonRuleSearch::to_json
- ::to_reprRuleSearch::to_repr
- ::to_jsonStatistics::to_json
- ::to_reprStatistics::to_repr
- ::newSystem::new
- ::equalTransition::equal
- ::from_jsonTransition::from_json
- ::not_equalTransition::not_equal
- ::to_jsonTransition::to_json
- ::to_reprTransition::to_repr
- ::eventVerificationCursor::event
- ::newVerificationCursor::new
- ::stagesVerificationCursor::stages
- ::submitVerificationCursor::submit
- ::to_reprVerificationEvent::to_repr
- ::to_reprVerificationPlan::to_repr
- ::to_jsonVerificationStage::to_json
- ::to_reprVerificationStage::to_repr
V
compare
V
confirm_difference
V
decode_model
V
diagnose_models
V
distinguish
V
evidence_html
V
learn
V
learn_with
V
regression_junit

moon-statelens

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

automata-learning

mealy

model-inference

testing

Download zip

Author

CaptainK-65

Version

0.3.0

License

Apache-2.0

Repository

github.com/CaptainK-65/moon-statelens

Last updated

8 days ago

Downloads

260

#Tested embedding example

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

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

Model-derived regression suites retain every original assertion when sharing prefixes. Independent fresh stability probes remain enabled by default:

///|
test "saved assertions and successful-event safety rules" {
  let model = @lens.Machine::new(["logout", "request"], [
    [{ target: 0, output: "ok", }, { target: 0, output: "denied", }],
  ])
  let suite = model.regression_suite(profile="wp", state_bound=1)
  let imported = @lens.RegressionSuite::from_json(Json(suite))
  assert_true(imported.plan().validate())
  let report = imported
    .plan()
    .run(@lens.Experiment::new(model.system(), model.alphabet()))
  guard report is { "passed": True, .. } else { fail("regression") }
  let rule = @lens.BehaviorRule::new(
    "logged-out-denial",
    { input: "request", output: "allowed", },
    kind="after",
    trigger={ input: "logout", output: "ok", },
  )
  assert_true(rule.search(model).witness is None)
  assert_eq(rule.check_trace(["logout", "request"], ["ok", "allowed"]), Some(1))
}

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(@moonbitlang/core/debug.Debug
Debug)

Invalid inputs, inconsistent observations and explicit resource limits.

LensError::to_repr

source

fn LensError::to_repr(LensError) -> @moonbitlang/core/debug.Repr
Repr

Algorithm

source

pub(all) enum Algorithm {
  LStar
  KearnsVazirani
} derive(Eq, @moonbitlang/core/debug.Debug
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

fn Algorithm::to_repr(Algorithm) -> @moonbitlang/core/debug.Repr
Repr

BehaviorRule

source

pub struct BehaviorRule {
  // private fields
}

A two-state safety monitor. On one step: release, trigger, then prohibition. Thus a successful release cancels a prohibition on that same step unless the step also matches the trigger. These are finite safety rules, not full LTL.

impl ToJson for BehaviorRule

BehaviorRule::check_trace

source

fn BehaviorRule::check_trace(self : BehaviorRule, inputs : Array[String], outputs : Array[String]) -> Int? raise LensError

First violating output position in a complete actual trace, starting at reset.

BehaviorRule::finding

source

fn BehaviorRule::finding(self : BehaviorRule, search : RuleSearch, actual : Array[String]?) -> Json raise

Assemble evidence from a complete reset-based replay; callers own its IO provenance.

BehaviorRule::from_json

source

fn BehaviorRule::from_json(value : Json) -> BehaviorRule raise

BehaviorRule::new

source

fn BehaviorRule::new(id : String, forbidden : RuleEvent, kind? : String, trigger? : RuleEvent, release? : RuleEvent) -> BehaviorRule raise LensError

kind is forbidden, after, or until. after/until require trigger; until also requires release. after/until start inactive after reset.

BehaviorRule::search

source

fn BehaviorRule::search(self : BehaviorRule, model : Machine, max_pairs? : Int) -> RuleSearch raise LensError

BFS over model × finite monitor. A witness is only a model prediction.

BehaviorRule::to_json

source

fn BehaviorRule::to_json(self : BehaviorRule) -> Json

BehaviorRule::verify

source

fn BehaviorRule::verify(self : BehaviorRule, model : Machine, experiment : Experiment, max_pairs? : Int) -> Json raise

No model witness means no fresh target confirmation, even after full search.

CheckResult

source

pub(all) enum CheckResult {
  Counterexample(Array[String])
  NoCounterexample(Evidence)
  Inconclusive(String)
} derive(@moonbitlang/core/debug.Debug
Debug)

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

CheckResult::to_repr

source

fn CheckResult::to_repr(CheckResult) -> @moonbitlang/core/debug.Repr
Repr

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(@moonbitlang/core/debug.Debug
Debug)

impl ToJson for CompatibilityResult

CompatibilityResult::to_json

source

fn CompatibilityResult::to_json(self : CompatibilityResult) -> Json

CompatibilityResult::to_repr

source

fn CompatibilityResult::to_repr(CompatibilityResult) -> @moonbitlang/core/debug.Repr
Repr

CompatibilityStatus

source

pub(all) enum CompatibilityStatus {
  ConfirmedDifference(Difference)
  NoDifferenceBetweenHypotheses
  Inconclusive(String)
  ReplayUnstable(side~ : String, word~ : Array[String], expected~ : Array[String], actual~ : Array[String])
} derive(@moonbitlang/core/debug.Debug
Debug)

impl ToJson for CompatibilityStatus

CompatibilityStatus::to_json

source

fn CompatibilityStatus::to_json(self : CompatibilityStatus) -> Json

CompatibilityStatus::to_repr

source

fn CompatibilityStatus::to_repr(CompatibilityStatus) -> @moonbitlang/core/debug.Repr
Repr

Difference

source

pub(all) struct Difference {
  inputs : Array[String]
  left_outputs : Array[String]
  right_outputs : Array[String]
} derive(Eq, ToJson, @moonbitlang/core/debug.Debug
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

fn Difference::to_repr(Difference) -> @moonbitlang/core/debug.Repr
Repr

DriverMetrics

source

pub(all) struct DriverMetrics {
  states : Int
  access_sequences : Int
  discriminators : Int
  table_cells : Int
  table_symbols : Int
  tree_nodes : Int
} derive(ToJson, @moonbitlang/core/debug.Debug
Debug)

DriverMetrics::to_json

source

fn DriverMetrics::to_json(DriverMetrics) -> Json

DriverMetrics::to_repr

source

fn DriverMetrics::to_repr(DriverMetrics) -> @moonbitlang/core/debug.Repr
Repr

Evidence

source

pub(all) enum Evidence {
  ExactReference
  ConditionalStateBound(Int)
  Budgeted(String)
} derive(@moonbitlang/core/debug.Debug
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

fn Evidence::to_repr(Evidence) -> @moonbitlang/core/debug.Repr
Repr

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

fn LearningDriver::metrics(self : LearningDriver) -> DriverMetrics

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(@moonbitlang/core/debug.Debug
Debug)

LearningEvent::to_repr

source

fn LearningEvent::to_repr(LearningEvent) -> @moonbitlang/core/debug.Repr
Repr

LearningResult

source

pub(all) struct LearningResult {
  model : Machine?
  status : LearningStatus
  statistics : Statistics
  rounds : Array[LearningRound]
  counterexamples : Array[Difference]
} derive(@moonbitlang/core/debug.Debug
Debug)

impl ToJson for LearningResult

LearningResult::to_json

source

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

LearningResult::to_repr

source

fn LearningResult::to_repr(LearningResult) -> @moonbitlang/core/debug.Repr
Repr

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, @moonbitlang/core/debug.Debug
Debug)

LearningRound::to_json

source

fn LearningRound::to_json(LearningRound) -> Json

LearningRound::to_repr

source

fn LearningRound::to_repr(LearningRound) -> @moonbitlang/core/debug.Repr
Repr

LearningStatus

source

pub(all) enum LearningStatus {
  Supported(Evidence)
  Inconclusive(String)
  Unstable(word~ : Array[String], expected~ : Array[String], actual~ : Array[String])
} derive(@moonbitlang/core/debug.Debug
Debug)

impl ToJson for LearningStatus

LearningStatus::to_json

source

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

LearningStatus::to_repr

source

fn LearningStatus::to_repr(LearningStatus) -> @moonbitlang/core/debug.Repr
Repr

Machine

source

pub struct Machine {
  // private fields
} derive(@moonbitlang/core/debug.Debug
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::regression_suite

source

fn Machine::regression_suite(self : Machine, profile? : String, state_bound? : Int, max_candidates? : Int, max_symbols? : Int, max_work? : Int) -> RegressionSuite raise

Generate deterministic suites; truncation is explicit, never a proof.

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

fn Machine::to_repr(Machine) -> @moonbitlang/core/debug.Repr
Repr

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.

ModelDiagnosis

source

pub(all) struct ModelDiagnosis {
  differences : Array[Difference]
  complete : Bool
  visited_pairs : Int
  checked_edges : Int
  reason : String?
} derive(ToJson, @moonbitlang/core/debug.Debug
Debug)

Bounded differing edges in the reachable product graph. Contexts need not be independent defects. State numbers are never assumed to align.

ModelDiagnosis::to_json

source

fn ModelDiagnosis::to_json(ModelDiagnosis) -> Json

ModelDiagnosis::to_repr

source

fn ModelDiagnosis::to_repr(ModelDiagnosis) -> @moonbitlang/core/debug.Repr
Repr

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(@moonbitlang/core/debug.Debug
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

fn QueryRequest::to_repr(QueryRequest) -> @moonbitlang/core/debug.Repr
Repr

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(@moonbitlang/core/debug.Debug
Debug)

QueryStart::to_repr

source

fn QueryStart::to_repr(QueryStart) -> @moonbitlang/core/debug.Repr
Repr

RegressionCase

source

pub(all) struct RegressionCase {
  inputs : Array[String]
  expected : Array[String]
} derive(Eq, ToJson, @moonbitlang/core/debug.Debug
Debug, @moonbitlang/core/json.FromJson
FromJson)

One independent reset-based experiment. Every output position is asserted.

RegressionCase::equal

source

fn RegressionCase::equal(RegressionCase, RegressionCase) -> Bool

RegressionCase::from_json

source

fn RegressionCase::from_json(Json, @moonbitlang/core/json.JsonPath
JsonPath) -> RegressionCase raise @moonbitlang/core/json.JsonDecodeError
JsonDecodeError

RegressionCase::not_equal

source

fn RegressionCase::not_equal(x : RegressionCase, y : RegressionCase) -> Bool

RegressionCase::to_json

source

fn RegressionCase::to_json(RegressionCase) -> Json

RegressionCase::to_repr

source

fn RegressionCase::to_repr(RegressionCase) -> @moonbitlang/core/debug.Repr
Repr

RegressionExecution

source

pub struct RegressionExecution {
  // private fields
}

IO-independent execution cursor shared by synchronous and asynchronous runners.

RegressionExecution::abort

source

fn RegressionExecution::abort(self : RegressionExecution, reason : String, unstable? : Bool) -> Unit

RegressionExecution::next_word

source

fn RegressionExecution::next_word(self : RegressionExecution) -> Array[String]?

Callers must execute every requested word with a fresh physical reset.

RegressionExecution::observe

source

fn RegressionExecution::observe(self : RegressionExecution, outputs : Array[String]) -> Unit raise

RegressionExecution::report

source

fn RegressionExecution::report(self : RegressionExecution) -> Json

RegressionPlan

source

pub struct RegressionPlan {
  // private fields
}

Every original case maps to a physical word whose output prefix asserts it. This changes reset scheduling under deterministic Mealy assumptions only.

RegressionPlan::alphabet

source

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

RegressionPlan::certificate

source

fn RegressionPlan::certificate(self : RegressionPlan) -> Json

RegressionPlan::execution

source

fn RegressionPlan::execution(self : RegressionPlan, stability_rechecks? : Int) -> RegressionExecution raise

RegressionPlan::run

source

fn RegressionPlan::run(self : RegressionPlan, experiment : Experiment, stability_rechecks? : Int) -> Json raise

Independent model mismatch is a regression, not proof of old/new real-target difference.

RegressionPlan::validate

source

fn RegressionPlan::validate(self : RegressionPlan) -> Bool raise

Independently verify each prefix and every expected output position.

RegressionPlan::words

source

fn RegressionPlan::words(self : RegressionPlan) -> Array[Array[String]]

RegressionSuite

source

pub struct RegressionSuite {
  // private fields
}

Validated, owned suite. Only completed W/Wp generation carries a conditional state-bound claim; state/transition profiles provide model coverage only.

impl ToJson for RegressionSuite

RegressionSuite::cases

source

fn RegressionSuite::cases(self : RegressionSuite) -> Array[RegressionCase]

RegressionSuite::coverage

source

fn RegressionSuite::coverage(self : RegressionSuite) -> Json

Coverage counts reachable model states/edges visited by the original suite.

RegressionSuite::evidence

source

fn RegressionSuite::evidence(self : RegressionSuite) -> Json

RegressionSuite::from_json

source

fn RegressionSuite::from_json(value : Json) -> RegressionSuite raise

Recompute the generator and evidence instead of trusting imported claims.

RegressionSuite::is_complete

source

fn RegressionSuite::is_complete(self : RegressionSuite) -> Bool

RegressionSuite::plan

source

fn RegressionSuite::plan(self : RegressionSuite, compact? : Bool) -> RegressionPlan

RegressionSuite::to_json

source

fn RegressionSuite::to_json(self : RegressionSuite) -> Json

RuleEvent

source

pub(all) struct RuleEvent {
  input : String
  output : String
} derive(Eq, ToJson, @moonbitlang/core/debug.Debug
Debug, @moonbitlang/core/json.FromJson
FromJson)

Rules match successful observable input/output events, not input names alone.

RuleEvent::equal

source

fn RuleEvent::equal(RuleEvent, RuleEvent) -> Bool

RuleEvent::from_json

source

fn RuleEvent::from_json(Json, @moonbitlang/core/json.JsonPath
JsonPath) -> RuleEvent raise @moonbitlang/core/json.JsonDecodeError
JsonDecodeError

RuleEvent::not_equal

source

fn RuleEvent::not_equal(x : RuleEvent, y : RuleEvent) -> Bool

RuleEvent::to_json

source

fn RuleEvent::to_json(RuleEvent) -> Json

RuleEvent::to_repr

source

fn RuleEvent::to_repr(RuleEvent) -> @moonbitlang/core/debug.Repr
Repr

RuleSearch

source

pub(all) struct RuleSearch {
  witness : Array[String]?
  search_complete : Bool
  visited_pairs : Int
  reason : String?
} derive(ToJson, @moonbitlang/core/debug.Debug
Debug)

RuleSearch::to_json

source

fn RuleSearch::to_json(RuleSearch) -> Json

RuleSearch::to_repr

source

fn RuleSearch::to_repr(RuleSearch) -> @moonbitlang/core/debug.Repr
Repr

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, @moonbitlang/core/debug.Debug
Debug)

Immutable counters. Attempts include target calls that fail.

Statistics::to_json

source

fn Statistics::to_json(Statistics) -> Json

Statistics::to_repr

source

fn Statistics::to_repr(Statistics) -> @moonbitlang/core/debug.Repr
Repr

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, @moonbitlang/core/debug.Debug
Debug, @moonbitlang/core/json.FromJson
FromJson)

One transition of a complete deterministic Mealy machine.

Transition::equal

source

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

Transition::from_json

source

fn Transition::from_json(Json, @moonbitlang/core/json.JsonPath
JsonPath) -> Transition raise @moonbitlang/core/json.JsonDecodeError
JsonDecodeError

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

fn Transition::to_repr(Transition) -> @moonbitlang/core/debug.Repr
Repr

VerificationCursor

source

pub struct VerificationCursor {
  // private fields
}

VerificationCursor::event

source

fn VerificationCursor::event(self : VerificationCursor) -> VerificationEvent raise LensError

VerificationCursor::new

source

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

VerificationCursor::stages

source

fn VerificationCursor::stages(self : VerificationCursor) -> Array[VerificationStage]

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(@moonbitlang/core/debug.Debug
Debug)

VerificationEvent::to_repr

source

fn VerificationEvent::to_repr(VerificationEvent) -> @moonbitlang/core/debug.Repr
Repr

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(@moonbitlang/core/debug.Debug
Debug)

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

VerificationPlan::to_repr

source

fn VerificationPlan::to_repr(VerificationPlan) -> @moonbitlang/core/debug.Repr
Repr

VerificationStage

source

pub(all) struct VerificationStage {
  strategy : String
  tests : Int
  result : String
} derive(ToJson, @moonbitlang/core/debug.Debug
Debug)

VerificationStage::to_json

source

fn VerificationStage::to_json(VerificationStage) -> Json

VerificationStage::to_repr

source

fn VerificationStage::to_repr(VerificationStage) -> @moonbitlang/core/debug.Repr
Repr

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

diagnose_models

source

fn diagnose_models(left : Machine, right : Machine, max_pairs? : Int, max_findings? : Int, max_edges? : Int) -> ModelDiagnosis raise LensError

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.

evidence_html

source

fn evidence_html(report : Json) -> String

Self-contained viewer. Target data lives in escaped inert text, never in a script literal or innerHTML. No network, CDN, tracking, or active target IO.

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.

regression_junit

source

fn regression_junit(report : Json) -> String raise LensError

CI consumes one testcase per original assertion plus an explicit failure when evidence is incomplete. Unknown formats are rejected.

Install

Download zip

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

automata-learningmealymodel-inferencetesting

CaptainK-65

Apache-2.0

github.com/CaptainK-65/moon-statelens

Updated 8 days ago

260 downloads

Site source Report issue Modules Skills CLI Build queue Statistics

moon-statelens

#Tested embedding example

#LensError

#LensError::to_repr

#Algorithm

#Algorithm::equal

#Algorithm::name

#Algorithm::not_equal

#Algorithm::to_repr

#BehaviorRule

#BehaviorRule::check_trace

#BehaviorRule::finding

#BehaviorRule::from_json

#BehaviorRule::new

#BehaviorRule::search

#BehaviorRule::to_json

#BehaviorRule::verify

#CheckResult

#CheckResult::to_repr

#CompatibilityResult

#CompatibilityResult::to_json

#CompatibilityResult::to_repr

#CompatibilityStatus

#CompatibilityStatus::to_json

#CompatibilityStatus::to_repr

#Difference

#Difference::equal

#Difference::not_equal

#Difference::to_json

#Difference::to_repr

#DriverMetrics

#DriverMetrics::to_json

#DriverMetrics::to_repr

#Evidence

#Evidence::to_json

#Evidence::to_repr

#Experiment

#Experiment::alphabet

#Experiment::new

#Experiment::query

#Experiment::statistics

#LearningDriver

#LearningDriver::algorithm

#LearningDriver::event

#LearningDriver::metrics

#LearningDriver::new

#LearningDriver::refine

#LearningDriver::result

#LearningDriver::submit

#LearningEvent

#LearningEvent::to_repr

#LearningResult

#LearningResult::to_json

#LearningResult::to_repr

#LearningRound

#LearningRound::to_json

#LearningRound::to_repr

#LearningStatus

#LearningStatus::to_json

#LearningStatus::to_repr

#Machine

#Machine::access_sequences

#Machine::alphabet

#Machine::characterizing_set

#Machine::distinguish_states

#Machine::encode

#Machine::from_json

#Machine::initial_state

#Machine::minimize

#Machine::new

#Machine::regression_suite

#Machine::state_count

#Machine::system

#Machine::table

#Machine::to_dot

#Machine::to_json

#Machine::to_repr

#Machine::trace

#Machine::trace_from

#ModelDiagnosis

LensError

LensError::to_repr

Algorithm

Algorithm::equal

Algorithm::name

Algorithm::not_equal

Algorithm::to_repr

BehaviorRule

BehaviorRule::check_trace

BehaviorRule::finding

BehaviorRule::from_json

BehaviorRule::new

BehaviorRule::search

BehaviorRule::to_json

BehaviorRule::verify

CheckResult

CheckResult::to_repr

CompatibilityResult

CompatibilityResult::to_json

CompatibilityResult::to_repr

CompatibilityStatus

CompatibilityStatus::to_json

CompatibilityStatus::to_repr

Difference

Difference::equal

Difference::not_equal

Difference::to_json

Difference::to_repr

DriverMetrics

DriverMetrics::to_json

DriverMetrics::to_repr

Evidence

Evidence::to_json

Evidence::to_repr

Experiment

Experiment::alphabet

Experiment::new

Experiment::query

Experiment::statistics

LearningDriver

LearningDriver::algorithm

LearningDriver::event

LearningDriver::metrics

LearningDriver::new

LearningDriver::refine

LearningDriver::result

LearningDriver::submit

LearningEvent

LearningEvent::to_repr

LearningResult

LearningResult::to_json

LearningResult::to_repr

LearningRound

LearningRound::to_json

LearningRound::to_repr

LearningStatus

LearningStatus::to_json

LearningStatus::to_repr

Machine

Machine::access_sequences

Machine::alphabet

Machine::characterizing_set

Machine::distinguish_states

Machine::encode

Machine::from_json

Machine::initial_state

Machine::minimize

Machine::new

Machine::regression_suite

Machine::state_count

Machine::system

Machine::table

Machine::to_dot

Machine::to_json

Machine::to_repr

Machine::trace

Machine::trace_from

ModelDiagnosis

ModelDiagnosis::to_json

ModelDiagnosis::to_repr