-
Notifications
You must be signed in to change notification settings - Fork 1
/
solver-help.maude
15 lines (15 loc) · 1.06 KB
/
solver-help.maude
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
fmod SOLVER-HELP is
pr FM-EXT-QID-LIST .
op solver-help : -> QidList .
eq solver-help
= '\b string2qidList("SOLVER - Additional commands available:") '\o '\n
'\t string2qidList("(initialize[<module>, <initState>, <leadsToFormula>, <eventuallyFormula>, <elementSort>, <soupSort>])") '\n
'\t '\t string2qidList("- LeadsTo property : set <leadsToFormula> to LeadsTo formula") '\n
'\t '\t string2qidList("- Eventually property : ignore <leadsToFormula> by setting it to ") '\n
'\t string2qidList("(layerCheck <NatList>)") '\s string2qidList("- given a list of depth at each layer for exploring") '\n
'\t string2qidList("(lastCheck)") '\s string2qidList("- checking at the last layer") '\n
'\t string2qidList("(check <NatList>)") '\s string2qidList("- combining layerCheck and lastCheck into one command") '\n
'\t string2qidList("(analyze)") '\s string2qidList("- showing current state") '\n
'\t string2qidList("(clear)") '\s string2qidList("- restoring to the initialization") '\n
'\t string2qidList("(solver-help)") '\n .
endfm