bmc

Documentation

Overview

Package bmc provides bounded model checking support.

Index

• type T
  • func New(s *logic.S, bads ...z.Lit) *T
  • func (t *T) DistributeTimeout(d time.Duration)
  • func (t *T) FillOutput(dst *reach.Output)
  • func (t *T) SetBadTimeout(bad z.Lit, d time.Duration)
  • func (t *T) SetMaxDepth(d int)
  • func (t *T) Try(dur time.Duration) int

Types

type T

type T struct {
	// contains filtered or unexported fields
}

T encapsulates a SAT based bounded model checker.

func New

func New(s *logic.S, bads ...z.Lit) *T

New creates a new bounded model checker for bad states `bads` occuring in `s`.

If `len(bads)==0`, then New panics.

func (*T) DistributeTimeout

func (t *T) DistributeTimeout(d time.Duration)

DistributeTimeout sets the timeout to `d`. If there are `N` bad states in t, then each bad state has timeout set to `d / N`.

func (*T) FillOutput

func (t *T) FillOutput(dst *reach.Output)

FillOutput fills the output object with bads and traces

func (*T) SetBadTimeout

func (t *T) SetBadTimeout(bad z.Lit, d time.Duration)

SetBadTimeout sets a timeout for the bad state `bad`.

SetBadTimeout panics if `bad` was not supplied as a bad state in the call to `New()` that created `t`.

func (*T) SetMaxDepth

func (t *T) SetMaxDepth(d int)

SetMaxDepth sets the maximum depth of subsequent bmc runs.

func (*T) Try

func (t *T) Try(dur time.Duration) int

Try tries to find paths to bad states within the constraints specified earlier (per bad timeout, max depth) and within duration `dur`.

Run returns the number of reachable bad states found.