verifier package

Submodules

verifier.LTL_property_base module

class verifier.LTL_property_base.LTLPropertyBase(LTL_str, penalty, enabled=True)

Bases: object

This is a base class that contains information of an LTL property.

It encapsulates the model-checking part (see check / check_incremental), and contains additional information. The subclass needs to describe specific APdict to be used.

APdict = None

The atomic propositions dict you must set in the subclass.

check(trace)

Checks the LTL property w.r.t. the given trace.

Parameters:trace – a sequence of states
Returns:result w.r.t. entire trace, in {TRUE, FALSE, UNDECIDED}
check_incremental(state)

Checks an initialised property w.r.t. the next state in a trace. Assumes init_property or check were previously called.

Parameters:state – next state (an integer)
Returns:incremental result, in {TRUE, FALSE, UNDECIDED}
parser = None

This property’s checker virtual machine

reset_property()

Resets existing property so that it can be applied to a new sequence of states.

Assumes init_property or check were previously called.

verifier.atomic_propositions_base module

class verifier.atomic_propositions_base.AtomicPropositionsBase

Bases: verifier.atomic_propositions_base.Bits

An AP-control base class for AP-wise manipulation.

the dictionary APdict and its length APdict_len has to be given in the subclass

APdict = None
class verifier.atomic_propositions_base.Bits(value=0)

Bases: object

A bit-control class that allows us bit-wise manipulation as shown in the example:

bits = Bits() bits[0] = False bits[2] = bits[0]

verifier.parser module

class verifier.parser.ErrorRec(l, c, s)

Bases: object

class verifier.parser.Errors

Bases: object

static Exception(errMsg)
static Init(fn, dir, merge, getParsingPos, errorMessages)
static SemErr(errMsg, errPos=None)
static Summarize(sourceBuffer)
static SynErr(errNum, errPos=None)
static Warn(errMsg, errPos=None)
count = 0
static display(s, e)
eof = False
errDist = 2
errMsgFormat = '%(file)s : (%(line)d, %(col)d) %(text)s\n'
errors = []
fileName = ''
listName = ''
mergeErrors = False
mergedList = None
minErrDist = 2
static printMsg(fileName, line, column, msg)
static storeError(line, col, s)
class verifier.parser.Parser

Bases: object

Check(trace)

Checks an entire trace w.r.t.

an existing property Scanner. Includes ResetProperty, but not SetProperty.

CheckIncremental(state)

Checks a new state w.r.t.

an existing property Scanner. Constructs a trace from new states using a new or previous trace list. If a previous trace list is used, states after index self.step are not valid.

Check_old(propscanner, trace)

Deprecated method to check an entire trace with a new property Scanner.

Includes SetProperty, which includes ResetProperty.

Conjunction(index)
Disjunction(index)
Expect(n)
ExpectWeak(n, follow)
FALSE = 0
Factor(index)
Get()
Implication(index)
LexString()
LookAheadString()
Parse(scanner)
Property(index)

Main property entry point.

PyCheck()

Unused dummy method.

ResetProperty()

Re-iniitializes an existing property Scanner.

SemErr(msg)
SetProperty(propscanner)

Sets the property Scanner that tokenizes the property.

StartOf(s)
Successful()
SynErr(errNum)
T = True
TRUE = 2
UNDECIDED = 1
UNDEFINED = -1
Warning(msg)
WeakSeparator(n, syFol, repFol)
errorMessages = {0: 'EOF expected', 1: 'proposition expected', 2: '"U" expected', 3: '"F" expected', 4: '"G" expected', 5: '"X" expected', 6: '"=>" expected', 7: '"or" expected', 8: '"and" expected', 9: '"not" expected', 10: '"true" expected', 11: '"false" expected', 12: '"(" expected', 13: '")" expected', 14: '??? expected', 15: 'invalid Property', 16: 'invalid Factor'}
getParsingPos()
maxT = 14
minErrDist = 2
set = [[True, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], [False, True, False, False, False, False, False, False, False, True, True, True, True, False, False, False]]
x = False

verifier.scanner module

class verifier.scanner.Buffer(s)

Bases: object

EOF = 'Ā'
Peek()
Read()
ReadChars(numBytes=1)
getPos()
getString(beg, end)
readPosition(pos)
setPos(value)
class verifier.scanner.Position(buf, beg, len, col)

Bases: object

getSubstring()
class verifier.scanner.Scanner(s)

Bases: object

CheckLiteral()
Comment0()
EOL = '\n'
NextCh()
NextToken()
Peek()
ResetPeek()
Scan()
charSetSize = 256
eofSym = 0
maxT = 14
noSym = 14
start = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -1]
class verifier.scanner.Token

Bases: object

Module contents