simasm 0.2.5

Abstract State Machine Framework for Discrete Event Simulation

SimASM

Abstract State Machine Framework for Discrete Event Simulation

SimASM is a Python package for modeling, simulating, and verifying discrete event systems using Abstract State Machines (ASM) as a common semantic foundation.

Features

• DSL for Simulation Models: Write discrete event simulation models in a clean, readable syntax
• Multiple Formalisms: Support for Event Graph and Activity Cycle Diagram modeling styles
• Stutter Equivalence Verification: Formally verify that two models produce equivalent observable behavior
• Jupyter Integration: Interactive modeling with %%simasm magic commands
• Statistics Collection: Built-in support for time-average, utilization, and count statistics

Installation

pip install simasm

For Jupyter support:

pip install simasm[jupyter]

Quick Start

In Jupyter/Colab

import simasm  # Auto-registers %%simasm magic

Define a model:

%%simasm model --name mm1_queue
domain Event
domain Load

var sim_clocktime: Real
var queue: List<Load>

// ... model definition

Run an experiment:

%%simasm experiment
experiment MyExperiment:
    model := "mm1_queue"

    replication:
        count: 10
        warm_up_time: 100.0
        run_length: 1000.0
    endreplication

    statistics:
        stat AvgQueueLength: time_average
            expression: "lib.length(queue)"
        endstat
    endstatistics
endexperiment

From Python

from simasm.experimenter.engine import ExperimenterEngine

# Run an experiment
engine = ExperimenterEngine("experiments/my_experiment.simasm")
result = engine.run()

print(f"Average queue length: {result['L_queue']}")

Model Syntax

SimASM uses a domain-specific language for defining simulation models:

// Domain declarations
domain Load
domain Server

// Constants and variables
const server: Server
var sim_clocktime: Real
var queue: List<Load>

// Random stream variables
var interarrival_time: rnd.exponential(1.25) as "arrivals"
var service_time: rnd.exponential(1.0) as "service"

// Rules
rule arrive() =
    let load = new Load
    lib.add(queue, load)
    // Schedule next arrival
endrule

// Main rule
main rule main =
    if sim_clocktime < sim_end_time then
        run_routine()
    endif
endrule

// Initial state
init:
    sim_clocktime := 0.0
    queue := []
endinit

Verification

SimASM can verify stutter equivalence between two models:

%%simasm verify
verification EG_vs_ACD:
    models:
        import EG from "event_graph_model.simasm"
        import ACD from "acd_model.simasm"
    endmodels

    seed: 42

    labels:
        label queue_empty for EG: "queue_count() == 0"
        label queue_empty for ACD: "queue_count() == 0"
    endlabels

    observables:
        observable queue_empty:
            EG -> queue_empty
            ACD -> queue_empty
        endobservable
    endobservables

    check:
        type: stutter_equivalence
        run_length: 1000.0
    endcheck
endverification

Documentation

• Full Documentation
• Examples

License

MIT License - see LICENSE for details.

Citation

If you use SimASM in your research, please cite:

@software{simasm,
  title = {SimASM: Abstract State Machine Framework for Discrete Event Simulation},
  author = {Steve},
  year = {2024},
  url = {https://github.com/yourusername/simasm}
}