WP Main Services

plugins.wp.goal (DATA)

Proof Obligations

goal ::= $wpo

plugins.wp.prover (DATA)

Prover Identifier

prover ::= $prover

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.getAvailableProvers (GET)

Returns the list of configured provers from why3

input ::= null

output ::= prover []

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.
"property" marker Property Marker
"fct" (opt.) fct Associated function, if any
"bhv" (opt.) string Associated behavior, if any
"thy" (opt.) string Associated axiomatic, 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
"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.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