tablemodel

type Action struct {
	Verb  string
	Args  []string
	Actor string
}

type Bind struct{ Cell, Target Cell }

type CannotRun struct{ Err error }

type Cell struct {
	P        Phys
	Row, Col string
}

type Datum struct {
	Cell   Cell
	Member string
	Score  int
}

type Event map[string]string

type Failure struct{ Msg string }

type Finding struct {
	Name   string
	Result string
	Text   string
}

type Location struct {
	P    Phys
	Cell Cell
}

type Phys struct {
	Table string
	Epoch int
}

type Placement struct {
	Member    string
	Locations []Location
}

type ReplayEvent struct {
	Step    string   // capture, receipt-replay, mutation-controls, tlc-execution, tlc-mutated-observation
	Verdict string   // pass, or expected-mutation-failure
	Fields  []string // key=value details
}

type ReplayOptions struct {
	Source string // the table.lua under test
	Jar    string // the TLC jar
	Java   string // the java program
	Models string // the directory of the TLA+ modules
	Dir    string // output directory: trace.json, the harness and the TLC logs
	Budget time.Duration

	Server ServerOptions
	Exec   tlc.Executor // tlc.Execute when nil
	OnStep func(ReplayEvent)
}

type RowAt struct {
	P   Phys
	Row string
}

type Server struct {
	Dir    string
	Socket string
	// contains filtered or unexported fields
}

type ServerOptions struct {
	RedisServer string        // the redis-server program
	TmpDir      string        // where the store's directory goes; the system default when empty
	Startup     time.Duration // how long the store has to create its socket
}

type State struct {
	Live   []Phys         `json:"live"`
	Rows   []RowAt        `json:"rows"`
	Binds  []Bind         `json:"binds"`
	Data   []Datum        `json:"data"`
	Place  []Placement    `json:"place"`
	Active int            `json:"active"`
	Seen   map[string]int `json:"seen"`
}

type Step struct {
	Name     string // configuration base name: MCTableMachine
	Module   string // the module file: MCTableMachine.tla
	Workers  int    // TLC workers
	Kind     string // pass, invariant or action
	Property string // the violated name for invariant and action
	Met      string // the verdict a met expectation is called
}

type StepOptions struct {
	Jar    string        // the TLC jar
	Java   string        // the java program
	Models string        // the directory of the modules and configurations
	Dir    string        // output directory: logs and the private copy of the models
	Budget time.Duration // the whole run's limit
	Exec   tlc.Executor  // tlc.Execute when nil
	OnStep func(StepResult)
}

type StepResult struct {
	Step    Step
	Verdict string
	OK      bool
	Code    int
	Seconds time.Duration
	Outcome tlc.Outcome
	Log     string
}

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

type Trace struct {
	SourceSHA256 string            `json:"source_sha256"`
	ModelSHA256  map[string]string `json:"model_sha256"`
	Initial      State             `json:"initial"`
	Steps        []TraceStep       `json:"steps"`
}

type TraceStep struct {
	Verb    string   `json:"verb"`
	Args    []string `json:"args"`
	Actor   string   `json:"actor"`
	Refused *bool    `json:"refused"`
	Receipt Event    `json:"receipt"`
	Model   string   `json:"model"`
	State   State    `json:"state"`
}