verifier package¶
Subpackages¶
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)¶
-
static
-
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.
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