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
- quot1.P: Quotienting rules (for better space usage, may lead to higher overall time usage)
- mgen.P: Model generation rules are present here
- nbisim.P: bisimulation based reduction for graphs
- catmouse.P: cat-mouse example with the formula
- catmouse1.P: Same example (to go with quot1.P, formula syntax is slightly different, see below)
Formula syntax (Version 1)
If you are using quot.P for better time usage, use the following 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. Version 1 will be removed eventually)
Formula syntax (Version 2)
If you are using quot1.P for better space usage, use the following formula syntax:
νx.(μy.(<b>tt \/ <c>y) /\ [a]x)
will be written as XSB fact
fDef(x, nu, and( fDef(y), fBox(a, form(x)))).
fDef(y, mu, or(fDiam(b, true), fDiam(c, form(y)))).
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 either btime or bspace to compile the files necessary for performing quotienting in less
time or space respectively.
| ?- btime.
[quot loaded]
[mgen loaded]
[nbisim loaded]
yes
Dynamically load the example file containing the "trans" relations for the plant model
and the specification given in terms of "fDef". If you use "bspace" above, you should
load "catmouse1".
| ?- 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(0),m5,s(1)).
transition1(s(0),c3,s(7)).
transition1(s(1),m6,s(2)).
transition1(s(1),c3,s(6)).
transition1(s(2),m4,s(0)).
transition1(s(2),m1,ff).
transition1(s(2),c3,ff).
transition1(s(6),m6,ff).
transition1(s(6),c1,ff).
transition1(s(6),c4,ff).
transition1(s(7),m5,s(6)).
transition1(s(7),c1,s(9)).
transition1(s(7),c4,s(10)).
transition1(s(9),hat(c7),s(10)).
transition1(s(9),m5,ff).
transition1(s(9),c2,s(0)).
transition1(s(10),hat(c7),s(9)).
transition1(s(10),m5,ff).
transition1(s(10),c5,ff).
yes
| ?-