modelchecker

README

FizzBee Model Checker Library

This package provides a minimal library interface for running FizzBee model checker simulations from Go code.

Features

• Run single simulation with specific seed
• No command-line flags or filesystem dependencies
• In-memory state graph results
• Pre-initialization hook support

Usage

For Bazel Projects

In your WORKSPACE file, add the fizzbee repository:

# Option 1: Using http_archive (for released versions)
load("@bazel_tools//tools/build_defs/repo:http.bzl", "http_archive")

http_archive(
    name = "fizzbee",
    urls = ["https://github.com/fizzbee-io/fizzbee/archive/refs/tags/v0.x.x.tar.gz"],
    strip_prefix = "fizzbee-0.x.x",
    # sha256 = "...",
)

# Option 2: Using local_repository (for development)
local_repository(
    name = "fizzbee",
    path = "/path/to/fizzbee",
)

# Option 3: Using git_repository (for latest)
load("@bazel_tools//tools/build_defs/repo:git.bzl", "git_repository")

git_repository(
    name = "fizzbee",
    remote = "https://github.com/fizzbee-io/fizzbee.git",
    branch = "main",  # or specific tag/commit
)

In your BUILD file:

load("@rules_go//go:def.bzl", "go_binary", "go_library")

go_library(
    name = "mylib",
    srcs = ["main.go"],
    deps = [
        "@fizzbee//pkg/modelchecker",
    ],
)

For Standard Go Projects

go get github.com/fizzbee-io/fizzbee/pkg/modelchecker

Example

package main

import (
    "fmt"
    "os"

    "github.com/fizzbee-io/fizzbee/pkg/modelchecker"
)

func main() {
    // Load your spec (JSON AST format)
    specData, err := os.ReadFile("spec_ast.json")
    if err != nil {
        panic(err)
    }

    // Configure the simulation
    config := &modelchecker.SimulationConfig{
        Seed:        12345,
        PreinitHook: "x = 10",  // Optional: set initial values
    }

    // Run the simulation
    result := modelchecker.RunSimulation(specData, config)
    if result.Error != nil {
        panic(result.Error)
    }

    // Check results
    if result.FailedNode != nil {
        fmt.Println("Invariant violation found!")
        fmt.Printf("Failed at state: %v\n", result.FailedNode)
    } else {
        fmt.Println("No violations found")
    }

    // Access the state graph
    fmt.Printf("Initial state: %v\n", result.InitNode)
}

API Reference

RunSimulation(specData []byte, config *SimulationConfig) *SimulationResult

Runs a single model checking simulation.

Parameters:

• specData: JSON AST representation of your FizzBee specification
• config: Configuration options (can be nil for defaults)

Returns:

• SimulationResult containing the state graph and any failures

SimulationConfig

Configuration for simulation runs:

type SimulationConfig struct {
    Seed        int64   // Random seed (0 = use timestamp)
    PreinitHook string  // Starlark code to run before init
    Options     *ast.StateSpaceOptions  // State space options
    DirPath     string  // Directory for loading modules
}

SimulationResult

Results from a simulation:

type SimulationResult struct {
    InitNode   *modelchecker.Node  // Root of state graph
    FailedNode *modelchecker.Node  // Node where invariant failed (nil if success)
    Error      error               // Any error during simulation
}

Advanced Usage

With State Space Options

import ast "fizz/proto"

options := &ast.StateSpaceOptions{
    MaxActions: proto.Int64(1000),
    MaxConcurrentActions: proto.Int32(10),
}

config := &modelchecker.SimulationConfig{
    Seed:    42,
    Options: options,
}

result := modelchecker.RunSimulation(specData, config)

Loading Spec from JSON

file, err := modelchecker.LoadSpecFromJSON(specData)
if err != nil {
    panic(err)
}
// Use file.Actions, file.Invariants, etc.

Notes

• This library uses the existing modelchecker.Processor under the hood
• State graphs are kept in memory - for large state spaces, consider running as CLI
• For multiple simulation runs with different seeds, call RunSimulation multiple times
• The library is safe for concurrent use (each call creates a new Processor)

Differences from CLI

The library interface:

• ✅ Does NOT touch the filesystem (except for module loading if DirPath is set)
• ✅ Does NOT parse command-line flags
• ✅ Returns in-memory results instead of writing files
• ✅ Allows programmatic access to the state graph
• ❌ Does NOT support composition or refinement checking (yet)
• ❌ Does NOT generate DOT files or HTML reports automatically
• ❌ Does NOT create output directories

If you need these features, you can:

1. Use the existing modelchecker package directly (more complex API)
2. Use the CLI tool and parse its output files
3. Contribute to extend this library!

Documentation

Overview

Package modelchecker provides a simple library interface for running FizzBee simulations.

Index

• func LoadSpecFromJSON(data []byte) (*ast.File, error)
• type SimulationConfig
• type SimulationResult
  • func RunSimulation(specData []byte, config *SimulationConfig) *SimulationResult
• type VisitedMapTracking

Functions

func LoadSpecFromJSON

func LoadSpecFromJSON(data []byte) (*ast.File, error)

LoadSpecFromJSON is a convenience function to load a spec from JSON bytes

Types

type SimulationConfig

type SimulationConfig struct {
	// Seed for random number generation (0 = use timestamp)
	Seed int64

	// PreinitHook is Starlark code to run before initialization
	PreinitHook string

	// Options for state space exploration (nil = use defaults)
	Options *ast.StateSpaceOptions

	// DirPath is the directory for loading modules (empty = no modules)
	DirPath string

	// VisitedMapTracking controls loop detection behavior
	// Default: uses liveness-based logic
	// Enabled: always track visited states
	// Disabled: always clear visited map (no loop detection)
	VisitedMapTracking VisitedMapTracking
}

SimulationConfig contains configuration for a single simulation run

type SimulationResult

type SimulationResult struct {
	// InitNode is the root node of the state graph
	InitNode *modelchecker.Node

	// FailedNode is the node where an invariant failed (nil if no failure)
	FailedNode *modelchecker.Node

	// Error is any error that occurred during simulation
	Error error
}

SimulationResult contains the results of a simulation run

func RunSimulation

func RunSimulation(specData []byte, config *SimulationConfig) *SimulationResult

RunSimulation performs a single simulation run on the given specification. This is a minimal wrapper around the existing Processor for library use.

Example:

specData := []byte(`{"actions": [...]}`) // JSON AST
result := modelchecker.RunSimulation(specData, &modelchecker.SimulationConfig{
    Seed: 12345,
    PreinitHook: "initial_value = 10",
})
if result.FailedNode != nil {
    fmt.Println("Invariant violation found!")
}

type VisitedMapTracking

type VisitedMapTracking int

VisitedMapTracking controls whether the visited map should track visited states

const (
	// VisitedMapTrackingDefault uses the current logic based on liveness settings
	VisitedMapTrackingDefault VisitedMapTracking = 0
	// VisitedMapTrackingEnabled always tracks visited states (don't clear the map)
	VisitedMapTrackingEnabled VisitedMapTracking = 1
	// VisitedMapTrackingDisabled always clears the map (no loop detection)
	VisitedMapTrackingDisabled VisitedMapTracking = 2
)