libmc

libmc is a python module providing a collection of tools for KV Model Checking and implements the following concepts presented in the lecture.

Table of Contents

• Automata
  • Labelled Transition Systems
  • Finite Automata
  • Acceptance
  • Completeness and Determinism
  • Product
  • Sub-Set Construction
  • Complement
  • Traces
  • Conformance
  • Simulation
    • Weak Simulation
    • Bisimulation
  • Minimization
  • Asynchronous Composition
    • Partial Order Reduction
  • Visualization
    • DOT
    • TikZ
    • Highlighting Paths
• Reachability Analysis
  • BFS and DFS
  • Tarjan’s Algorithm
• Binary Decision Diagrams
  • Constants
  • Variables
  • Operators
  • Visualization
• Boole Parser
  • Format
  • Parsing
  • Evaluation
  • Conversion
    • To AIG
    • To BDD
• API

API Index

See Index for a list of module members.

Warning

This module has been implemented just for fun and educational purposes! Unfortunately there was no time to test it rigorously, so there might be bugs. Please feel free to report an issue for initiating pest control if you find one ;)