edu.ksu.cis.projects.bogor.module
Interface IStateAugmenter

All Superinterfaces:

Disposable, IModule

public interface IStateAugmenter
extends IModule

A hook to allow state manager "plugins" that transform the state vector after a vanilla version has been completely calculated. This is useful to, e.g., append automaton state ID's for a safety property checker.

Author:

Matt Hoosier

Method Summary

void	augmentState(IState s, BitBuffer bb) Manipulate the bit vector to encode some extra information.
FSM[]	getPropertyAutomata()
Location	getPropertyAutomatonState(FSM automaton, IState s)

Methods inherited from interface edu.ksu.cis.projects.bogor.module.IModule

connect, getCopyrightNotice, setOptions

Methods inherited from interface edu.ksu.cis.projects.bogor.util.Disposable

dispose

Method Detail

augmentState

void augmentState(IState s,
                  BitBuffer bb)

Manipulate the bit vector to encode some extra information.

Parameters:

s - current state

bb - vanilla version of bit vector

getPropertyAutomata

FSM[] getPropertyAutomata()

getPropertyAutomatonState

Location getPropertyAutomatonState(FSM automaton,
                                   IState s)