SCIFF Developer's Manual

SCIFF debugger

During the trace (not the CHR trace), it is possible to visualise the quantification of the variables.

If SICStus is trying to invoke a goal, e.g.:

Call: module:predicate(A,B,C)

to visualise the quantification of the variables, act as follows.

hit 'b' (break level)
invoke the goal: print_quant(module).
where 'module' is the name of the module of the predicate SICStus was going to Call.
If the module is not present, simply call print_quant.
exit from break level (^D in Linux, ^Z in Windows)

Moreover, the output of SCIFF during debugging can be saved in SVG format, and visualised in a browser. The trace of SICStus has been extended to support the command 'svg', that saves the output in the file debug.svg

graphviz

Represents the sciff derivation tree in form of a graph, using the graphviz software.

The file should be opened with init_graph(FileName,Stream), and, after the execution of the proof, it should be closed with close_graph. The produced file can be opened with DOT and converted in PostScript or other formats.

Default value is off.

ics

From a low-level point of view, the integrity constraints are represented as CHR constraints. If you want to add an IC which is not allowed by the parser, you have to:

state the quantification of all the variables that occur in the IC
invoke the IC.

in order to set the quantification of a variable X in an integrity constraint, invoke the goal forall(X) or exists(X).

The ic is represented as psic(Body,Head), where

Body is a list [H,NotH,E,NotE,En,NotEn,Abd,A], where H is a list of atoms h(Event,T), NotH is a list of noth(Event,T), E is a list of e(Event,T), NotE is a list of note(Event,T), En is a list of en(Event,T), NotEn is a list of noten(Event,T), Abd is a list of abd(Event,T), and A is a list of atoms.
Head is a list of lists. The list of lists represents a disjunction of conjunctions

remember that all the atoms have a Prolog syntax, i.e., they are lowercase (e.g., happened events are represented as h(Event,T))

For example, if you want to add the following IC:

H(p,Tp) → EN(q,Tq) ∧ E(r,Tr) ∨ E(s,Ts)

where for some reason you want Tq quantified existentially and Tr universally, you can invoke the goal:

forall(Tp), forall(Tr), exists(Tq), exists(Ts), psic([[h(p,Tp)],[],[],[],[],[],[],[]],[[en(q,Tq),e(r,Tr)],[e(s,Ts)]]).

Example:

?- forall(Tp), forall(Tr), exists(Tq), exists(Ts), psic([[h(p,Tp)],[],[],[],[],[],[],[]],[[en(q,Tq),e(r,Tr)],[e(s,Ts)]]), h(p,1). pending(en(q,_A)), pending(e(r,_B)), psic([[h(p,Tp)],[],[],[],[],[],[],[]],[[en(q,Tq),e(r,Tr)],[e(s,Ts)]]), h(p,1), en(q,_A), e(r,_B) ? ; pending(e(s,_A)), psic([[h(p,Tp)],[],[],[],[],[],[],[]],[[en(q,Tq),e(r,Tr)],[e(s,Ts)]]), h(p,1), e(s,_A) ? ; no

RuleML

SCIFF can use as ICs files also files represented in RuleML 0.9.

Moreover, SCIFF can convert ICs from the internal representation into RuleML, using the predicate save_ics_ruleml(FileName) in the module ruleml_parser.

For example, after opening a project (e.g., project(auction)), use the command

ruleml_parser:save_ics_ruleml('ic.ruleml').

to save the ICs in the project to a file ic.ruleml in RuleML format.

download_ics

The predicate download_ics/1 lets you download an ICS file from the web. The only parameter is the URL of the ICS file, given as string (i.e., with double quotes "") The ICS file can be either in the ICS syntax, or in RuleML. The ICS are then imposed (i.e., they are invoked).

indexing

SCIFF uses indexing on the main functor of events. For example, the main functor of


H(tell(S,R,ask(Quote)),T)

is tell. SCIFF selects the atoms (in the set of happened events) by means of the main functor. Thus, it is more efficient if the main functor is informative. For instance, the following history:


h(ask(anne,bob),1).

h(reply(bob,anne),2).

is dealt with more efficiently than


h(tell(anne,bob,ask),1).

h(tell(bob,anne,reply),2).

because the expectation e(ask(S,R),T) is checked only against the first atom, while e(tell(S,R,ask),T) is checked with both (and in the second, the check fails).

The same holds for e, en, abd.

Linda

SCIFF can communicate through the Linda library. Currently, two uses are envisaged:

unidirectional acquisition of the history through Linda
Communication between SCIFF processes

Unidirectional acquisition of the history

In this modality, SCIFF reads the history of events through Linda.

To use it, you should

Start a Linda Server, with the commands:
```
:- use_module(library('linda/server')).
:- linda.
```
Linda should output the address and port of the server.
In a separate process, load SCIFF and linda_his. Connect to the server with
```
:- linda_client(address:port).
```
In the file project.pl, redefine the run(_) predicate (and, possibly, run_open and run_closed) as follows:
```
run(_):- run_dyn(nonblocking).
```
Now, you can start another Linda client, and use:
- out(h(Event,Time)) to send an event
- out(close_history) to close the history

Communication between SCIFF processes

In this case, two (or more) processes (e.g., SCIFF agents) communicate through Linda.

To use it, you should

Start a Linda Server, with the commands:
```
:- use_module(library('linda/server')).
:- linda.
```
Linda outputs the address and port of the server.
In separate processes, load SCIFF and linda_his (one for each SCIFF process). Connect to the server with
```
:- linda_client(address:port).
```

In the file project.pl, redefine the run predicates as follows:

   run_open(_):- run_dyn_argument_directional(nonblocking).
   run_closed(_):- run_dyn_argument_directional_closed(nonblocking).

and define run(_) either as run_open(_) or as run_closed(_).

In the SOKB of the SCIFF agents you should define the predicate me/1, containing the unique name of the agent.

You can use the following primitives:

send_message(+Sender,+Receiver,+Content,-Time). Sends a message from Sender to Receiver. Time is bound to the time in which the message is actually sent (it is a global counter in Linda). The message will be received by the Receiver in the form
```
h(tell(Sender,Receiver,Content),Time)
```
ABD(finished_reasoning,_). It is an abducible abduced when SCIFF reaches the quiescence. Useful if you want to send messages only when the state of the proof is stable. E.g.:
```
ABD(finished_reasoning,_) /\ (...) ---> send_message(...)
```

The agents will process all the events, and then suspend waiting for further events. They will terminate with success when they receive the message

leave_dialogue.

(i.e., out(leave_dialogue)).

Solvers

SCIFF can use different constraint solvers. The default constraint solver is CLP(FD), on finite domains.

To change the solver used by SCIFF, you can edit the file solver.pl. Such file loads the solver that will be used by SCIFF; by default it contains

:- ensure_loaded(fd_solver).

Available solvers are currently:

fd_solver: solver on finite domains, based on local consistency.
r_solver: solver on the reals, based on the CLPQR solver of SICStus (see also SICStus documentation).

To use the r_solver you have to pay attention in the SOKB at the syntax of constraints and constant numbers. Concerning constraints, instead of A #< B you should write either {A < B} (note the curly braces) or the (advised) lt(A,B). Note that you can use lt(A,B) also for the FD solver, so using this syntax lets you run your application with either of the two solvers withour rewriting your SOKB. In ICs, all translations are dealt with automatically, so you need not to change your ICs. The available constraints are currently neq/2, lt/2, eq/2, gt/2, leq/2, geq/2; all accept expressions as arguments (e.g., neq(A+1,B) is a valid constraint).

Concerning numbers, the r_solver is a solver on reals. Note that in SICStus the real 10.0 does not unify with the integer 10. However, the forementioned constraints deal with both, so you can indifferently write eq(A,10) or eq(A,10.0): in both cases A will get the real value 10.0.

In general, you cannot unify a constrained variable with an integer. For example, the goal

eq(A,10), A=10. fails. Even worse, the following goal raises an error:

| ?- leq(A,10), A=10.
! Type error in argument 2 of = /2
! 'a real number' expected, but 10 found
! goal:  _135=10

To avoid such situations, use the eq constraint instead of unification. E.g., do not write:

p:- geq(A,0), q(A).
q(1).
q(2).

but:

p:- geq(A,0), q(A).
q(X):- eq(X,1).
q(X):- eq(X,2).

Memory considerations

Currently SCIFF does not reuse common sub-structures when copying a term (which happens quite often in the derivation), because this would take slightly more time.

However, if in your application you need to save as much memory as possible, you can try the following:

open file ccopy.pl
in the definition of predicate ccopy/4, uncomment the clause
```
ccopy(X,Y,Old,New):- ground(X),!,X=Y,Old=New.
```

help

A help file is an html file. Each of the topics is indexed with an anchor

The end of the topics is recognised when there is the next topics, i.e., another anchor <a name="next topic"></a> You can link to such anchors, e.g. with <a href="#topics name">topics name</a>

Please, in links use as text the same name as the anchor, as it is used by the help system of SCIFF.