DATA
)Proof Obligations
goal
::=
$wpo
DATA
)Prover Identifier
prover
::=
$prover
STATE
)Selected Provers
SIGNAL
)Signal for state provers
GET
)Getter for state provers
input
::=
null
output
::=
prover
[]
SET
)Setter for state provers
input
::=
prover
[]
output
::=
null
STATE
)Server Processes
SIGNAL
)Signal for state process
GET
)Getter for state process
input
::=
null
output
::=
number
SET
)Setter for state process
input
::=
number
output
::=
null
STATE
)Prover’s Timeout
SIGNAL
)Signal for state timeout
GET
)Getter for state timeout
input
::=
null
output
::=
number
SET
)Setter for state timeout
input
::=
number
output
::=
null
ARRAY
)Available Provers
SIGNAL
)Signal for array ProverInfos
DATA
)Data for array rows ProverInfos
ProverInfosData
::= {
fields…}
Field | Format | Description |
---|---|---|
"prover" |
prover |
Entry identifier. |
"name" |
string | Prover Name |
"version" |
string | Prover Version |
"descr" |
string | Prover Full Name (description) |
GET
)Data fetcher for array ProverInfos
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
prover
[] |
removed entries |
"updated" |
ProverInfosData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array ProverInfos
input
::=
null
output
::=
null
GET
)Tells whether the prover is interactive
input
::=
prover
output
::=
boolean
DATA
)interactive mode
InteractiveMode
::=
tags…
Tags | Value | Description |
---|---|---|
Batch | "batch" |
Batch |
Update | "update" |
Update |
Edit | "edit" |
Edit |
Fix | "fix" |
Fix |
Fixup | "fixup" |
FixUpdate |
STATE
)Enabled Counter Examples
SIGNAL
)Signal for state counterExamples
GET
)Getter for state counterExamples
input
::=
null
output
::=
boolean
SET
)Setter for state counterExamples
input
::=
boolean
output
::=
null
DATA
)Prover Result
result
::=
{
"descr"
:
string ,"cached"
:
boolean ,"verdict"
:
string ,"solverTime"
:
number ,"proverTime"
:
number ,"proverSteps"
:
number}
DATA
)Test Status
status
::=
$NORESULT
|$COMPUTING
|$FAILED
|$STEPOUT
|$UNKNOWN
|$VALID
|$PASSED
|$DOOMED
DATA
)Prover Result
stats
::=
{
"summary"
:
string ,"tactics"
:
number ,"proved"
:
number ,"total"
:
number}
ARRAY
)Generated Goals
SIGNAL
)Signal for array goals
DATA
)Data for array rows goals
goalsData
::= {
fields…}
Field | Format | Description |
---|---|---|
"wpo" |
goal |
Entry identifier. |
"marker" |
marker |
Associated Marker |
"scope" (opt.) |
decl |
Associated declaration, if any |
"property" |
marker |
Property Marker |
"fct" (opt.) |
string | Associated function name, if any |
"bhv" (opt.) |
string | Associated behavior name, if any |
"thy" (opt.) |
string | Associated axiomatic name, if any |
"name" |
string | Informal Property Name |
"smoke" |
boolean | Smoking (or not) goal |
"passed" |
boolean | Valid or Passed goal |
"status" |
status |
Verdict, Status |
"stats" |
stats |
Prover Stats Summary |
"proof" |
boolean | Proof Tree |
"script" (opt.) |
string | Script File |
"saved" |
boolean | Saved Script |
GET
)Data fetcher for array goals
input
::=
number
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"reload" |
boolean | array fully reloaded |
"removed" |
goal
[] |
removed entries |
"updated" |
goalsData
[] |
updated entries |
"pending" |
number | remaining entries to be fetched |
GET
)Force full reload for array goals
input
::=
null
output
::=
null
EXEC
)Generate RTE guards for the function
input
::=
marker
output
::=
null
EXEC
)Generate goals and run provers
input
::=
marker
output
::=
null
SIGNAL
)Proof Server Activity
GET
)Scheduled tasks in proof server
input
::=
null
output
::=
{
output…}
Output | Format | Description |
---|---|---|
"procs" |
number | Max parallel tasks |
"active" |
number | Active tasks |
"done" |
number | Finished tasks |
"todo" |
number | Remaining jobs |
signals
plugins.wp.serverActivity
SET
)Cancel all scheduled proof tasks
input
::=
null
output
::=
null