WP Main Services

plugins.wp.goal (DATA)

Proof Obligations

goal ::= $wpo

plugins.wp.prover (DATA)

Prover Identifier

prover ::= $prover

plugins.wp.provers (STATE)

Selected Provers

plugins.wp.signalProvers (SIGNAL)

Signal for state provers

plugins.wp.getProvers (GET)

Getter for state provers

input ::= null

output ::= prover []

plugins.wp.setProvers (SET)

Setter for state provers

input ::= prover []

output ::= null

plugins.wp.process (STATE)

Server Processes

plugins.wp.signalProcess (SIGNAL)

Signal for state process

plugins.wp.getProcess (GET)

Getter for state process

input ::= null

output ::= number

plugins.wp.setProcess (SET)

Setter for state process

input ::= number

output ::= null

plugins.wp.timeout (STATE)

Prover’s Timeout

plugins.wp.signalTimeout (SIGNAL)

Signal for state timeout

plugins.wp.getTimeout (GET)

Getter for state timeout

input ::= null

output ::= number

plugins.wp.setTimeout (SET)

Setter for state timeout

input ::= number

output ::= null

plugins.wp.ProverInfos (ARRAY)

Available Provers

plugins.wp.signalProverInfos (SIGNAL)

Signal for array ProverInfos

plugins.wp.ProverInfosData (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)

plugins.wp.fetchProverInfos (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

plugins.wp.reloadProverInfos (GET)

Force full reload for array ProverInfos

input ::= null

output ::= null

plugins.wp.result (DATA)

Prover Result

result ::= { "descr" : string , "cached" : boolean , "verdict" : string , "solverTime" : number , "proverTime" : number , "proverSteps" : number }

plugins.wp.status (DATA)

Test Status

status ::= $NORESULT | $COMPUTING | $FAILED | $STEPOUT | $UNKNOWN | $VALID | $PASSED | $DOOMED

plugins.wp.stats (DATA)

Prover Result

stats ::= { "summary" : string , "tactics" : number , "proved" : number , "total" : number }

plugins.wp.goals (ARRAY)

Generated Goals

plugins.wp.signalGoals (SIGNAL)

Signal for array goals

plugins.wp.goalsData (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

plugins.wp.fetchGoals (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

plugins.wp.reloadGoals (GET)

Force full reload for array goals

input ::= null

output ::= null

plugins.wp.generateRTEGuards (EXEC)

Generate RTE guards for the function

input ::= marker

output ::= null

plugins.wp.startProofs (EXEC)

Generate goals and run provers

input ::= marker

output ::= null

plugins.wp.serverActivity (SIGNAL)

Proof Server Activity

plugins.wp.getScheduledTasks (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.cancelProofTasks (SET)

Cancel all scheduled proof tasks

input ::= null

output ::= null