Quotienting
Installation Instruction
The Qoutienting and model generation tool is written XSB logic
programming engine. To install and use the tool follow the steps
below:
-
Download XSB (tar) or get XSB2.6 from sourceforge (make sure xsb is
present in your path)
-
Source code for quotienting and model generation tool is available here.
The package has the following files:
- control.P: Top level file which ties all the other files
- quot.P: Quotienting rules are present here
- mgen.P: Model generation rules are present here
- nbisim.P: bisimulation based reduction for graphs
- formulaequiv.P: checking and removing equivalent formula expressions
- catmouse.P: cat-mouse example with the formula
Formula syntax
νx.(μy.(<b>tt \/ <c>y) /\ [a]x)
will be written as XSB facts
fDef(x, nu, and( fDef(y, mu, or(fDiam(b, true), fDiam(c, form(y)))), fBox(a, form(x)))).
fDef(y, mu, or(fDiam(b, true), fDiam(c, form(y)))).
(Don't forget the "." at the end)
How to execute
Once XSB is installed and its executable "xsb" is present in the path, execute as follows:
$ xsb
[xsb_configuration loaded]
[sysinitrc loaded]
[packaging loaded]
XSB Version 2.6 (Duff) of June 24, 2003
[i686-pc-cygwin; mode: optimal; engine: slg-wam; gc: indirection; scheduling: local]
| ?-
You have not entered xsb environment. Compile the file control.P
| ?- [control].
[control loaded]
yes
use btime to load all the necessary files. We will eventually release another version
which will load files necessary for low memory usage.
| ?- btime.
[quot loaded]
[mgen loaded]
[nbisim loaded]
[formulaequiv loaded]
yes
Dynamically load the example file containing the "trans" relations for the plant model
and the specification given in terms of "fDef".
| ?- load(catmouse).
[/cygdrive/c/research/projects/control/catmouse.P dynamically loaded, cpu time used: 0.0190 seconds]
yes
Finally, you can get a supervisor controller. Use the name of the formula variable as
argument for "getcontroller".
| ?- getcontroller(x).
transition1(s(45),m5,s(46)).
transition1(s(45),c3,s(49)).
transition1(s(46),m6,s(47)).
transition1(s(46),c3,s(47)).
transition1(s(47),m4,s(45)).
transition1(s(49),m5,s(50)).
transition1(s(49),c1,s(51)).
transition1(s(49),c4,s(51)).
transition1(s(51),c7,s(51)).
transition1(s(51),c2,s(45)).
yes
| ?-