SCIFF User's Manual

To get help, type help(topic) at the SICStus prompt. To get help on help, type help(help).

Help available on the following topics:


Getting Started

To run SCIFF, you can either use projects (preferred) or use low-level interface, explained in the following.

Create a directory with a name (say 'name') containing the following files:

call the goal: 'build(name)'

recompile SCIFF

call either 'run.' or 'run_no_close.'


Using Projects

In order to create a new project:

Now you can build the project, calling the goal
project(myprj).
and run it with run(X), or run_close(X).

See also project, run, run_open, run_close

run

run/1 is the predicate that runs a project.

The argument is currently not bound by default. By default, this predicate runs SCIFF in a closed derivation (see run_closed). The developer of the project can redefine this predicate in the project file (see projects) and use the parameter for input or output.

run_closed

run_closed/1 runs a project with a closed derivation.

The argument is currently not bound by default. The developer of the project can redefine this predicate in the project file (see projects) and use the parameter for input or output.

SCIFF can be run either with a closed or with an open derivation.

To run SCIFF with an open derivation, use run_open

run_open

run_open/1 runs a project with an open derivation.

The argument is currently not bound by default. The developer of the project can redefine this predicate in the project file (see projects) and use the parameter for input or output.

SCIFF can be run either with a closed or with an open derivation.

To run SCIFF with a closed derivation, use run_closed

project/1

The predicate project(name) builds a project called 'name'.

There must exist a corresponding directory called 'name', as a subdirectory of the default_dir and it must contain a file called project.pl

Such file should be created as explained in section projects

default_dir

The default directory where SCIFF looks for projects is declared in the file defaults.pl This file contains a fact default_dir that contains the path of the directory containing projects. By defult, it is the father of the directory containing SCIFF; i.e., by default defaults.pl contains default_dir('../').


Options

The following options are recognised by the SCIFF proof-procedure:

Options can be stated in projects by adding to the file project.pl a fact required_option/2. For example, if your project requires the option seq_act, add to the corresponding project.pl the fact:

required_option(seq_act,on).

To set an option, use set_option

To read the state of an option, use get_option or show_options.


fulfiller

fulfiller option enables the MarcoA's rule for generating histories (g-SCIFF). This option should be set off unless you are using the g-SCIFF.

seq_act

seq_act option imposes that two events cannot happen at the same time.

If seq_act is on, two events cannot happen at the same time.

If seq_act is off, more events can happen at the same time.

This option is primarily used in the Abductive Event Calculus.

Usually is off.

factoring

The factoring option enables or disables the factoring transition. The factoring transition tries and unifies two abduced atoms. On backtracking, the two abducibles are dis-unified. The factoring transition is useful for obtaining minimal answers. It is important for the Abductive Event Calculus.

The factoring option is off by default.

sciff_debug

Print on screen debug messages.

Usually is off.

violation_causes_failure

The option violation_causes_failure Decides if a violation of the protocol should induce a failure (and backtracking where possible) of the proof. Allowed values are yes/no. Default value is yes.

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.

allow_events_not_expected

By default, SCIFF allows events to happen even if they are not expected. By setting the allow_events_not_expected option to no, SCIFF detects as violation if an happened event does not have a corresponding expectation.

Useful, in particular, to prove Strong Conformance in the allows framework.

Default value is yes.

min_viol_closed

min_viol_closed/1,

amongst the various branches selects the one with the minimal number of violations. Returns the number of violations. Useful when used in conjunction with the option violation_causes_failure → no.

Known bug: the number of violations is not precise: often the reported number of violations should be increased by 1.

min_viol_open

Amongst the various branches selects the one with the minimal number of violations. Returns the number of violations. Useful when used in conjunction with the option violation_causes_failure → no.

Known bug: the number of violations is not precise: often the reported number of violations should be increased by 1.

set_option(Option,Value)

Each option can be set using the predicate:

set_option(Option,Value)

where Option is the name of the option you want to modify, and Value is the new value you want to assign to it.

See also get_option

get_option(Option,State)

You can inspect the state of an option using the predicate: sciff_option(?Option, ?State).

See also set_option

show_options

The predicate show_options shows all the options available and their state

See also get_option, set_option


Syntax of the history

The history should be in a text file, containing terms with a Functor and the following arguments:

The term should be terminated with full stop.

It will be converted into an atom

H(Functor(Sender,Receiver,Performative(Arguments),DialogID),Time).

Syntax of ICs

The ICs are the Integrity Constraints of the SCIFF proof-procedure. They are written in one (or more) text files that should be declared in the file project.pl (see projects) with a fact ics_file(Filename).

ICs are in the form of implications:

Body ---> Head
where Body is a conjunction of

Currently, the first literal in the Body must be of type H, E, EN, or ABD.

Head is a disjunction of conjunctions. Disjunctions are represented wih the symbol \/ , and conjunctions with /\ .

Each conjunct can be

For example, the following is a valid IC:

    % happened events
    H(tell(A,B,openauction(Item,TEnd,TDeadline),AuctionId),TOpen)
    /\ H(tell(B,A,bid(Item,Quote),AuctionId),TBid)
	/\ deadline(X) % Literal defined in SOKB
	/\ TOpen < TBid % CLP constraints
	/\ TOpen <= TEnd
	/\ TEnd < TDeadline+X
--->
	E(tell(A,B,answer(win,Item,Quote),AuctionId),TWin)
	/\ TWin <= TDeadline
	/\ TEnd < TWin
\/
	E(tell(A,B,answer(lose,Item,Quote),AuctionId),TLose)
	/\ TLose <= TDeadline
	/\ TEnd < TLose.

Comments are represented with the ampersand symbol (%) and terminate at the end of the line (as in Prolog). The IC terminates with a full stop.

As an alternative, ICs can also be defined in ruleml.

RuleML

As an alternative to the syntax of ics, it is possible to define the ICs with the syntax in RuleML 0.9.

RuleML files are declared in the project file with the same syntax of normal ICs files: using the ics_file/1 predicate. SCIFF will try to parse the file first as a RuleML file. In case of failure, it will use the normal ICs parser.


Syntax of SOKB

The SOKB is a set of clauses, a la logic programming. Each clause is an implication

head :- body.
where head is an atom and body is a conjunction of literals, that can contain abducibles and clp constraints.

The abducibles can be expectations or general abducibles. The syntax of abducibles is different from that of ics, and is the following:

The SOKB can be defined in one or more files. Each sokb file should be declared in the project.pl in a fact

sokb_file(Name_Of_SOKB_File).

Exactly one of the SOKB files should define the predicate society_goal/0. The predicate society_goal contains the goal of the society, that is the starting point of SCIFF derivation. society_goal is invoked by the run, run_open and run_closed predicates that start the derivation.


CLP Constraints

Currently, the set of CLP constraints that are interpreted in the ics is the following:

as well as unification = and dis-unification !=


fdet declarations

In order to test if an E expectation is fulfilled by a H event, SCIFF generates two alternative hypotheses: in one it tries to prove that the two will unify, while in the second it tries and prove that they will not unify.

In some cases, the protocol specification might implicitly impose that all expectations of type

E(message(S,R,type),T)
can be fulfilled at most by one event. For instance, if in a protocol we have that
E(message(S1,R1,type),T1) ∧ E(message(S2,R2,type),T2) → S1=S2 ∧ R1=R2 ∧ T1=T2
then we know that only one event can fulfill an E expectation matching with
E(message(S,R,type),T).

In such cases, the performance can be improved by declaring such event as having deterministic fulfilment. This can be accomplished by adding to the SOKB a predicate fdet/1. In the example, add to the SOKB the definition:
fdet(e(message(S,R,type),T)).

Of course, if one E expectation can be matched by more than one H event, declaring it as fdet undermines completeness, i.e., some solutions may be lost.


AlLoWS

AlLoWS (Abductive Logic Web-service Specification) is a framework for testing conformance of web services to choreographies (see publication PPDP 2006).

In order to use AlLoWS, you have to

In AlLoWS, expectations are only positive (E) and have the following syntax:

E(do(Expecter,Sender,Receiver,Message,DialogID),Time)

where Expecter can be either chor (i.e., this is an expectation of the choreography), or the name of the web service under test (in the example, ws)

The society_goal should be defined only once (in either of the two SOKBs), and should contain the expectation, both from the choreography and from the web service's viewpoint, of the message that initiates the interaction. For example:

society_goal:-
 e(do(ws, peer,ws,m1,d1),1),
 e(do(chor,peer,ws,m1,d1),1).

Build the project, with the predicate project

Finally, you can execute the goal allows(Succeed), or redefine, in the file project.pl (see projects) the predicate run as follows:

run(Succeed) :- allows(Succeed).

If the web service is not conformant, AlLoWS provides, as counterexample, a possible history that does not satisfy either the web service's or the choreography's specifications.

The parameter Succeed is useful to drive the behaviour of the predicate allows/1.

AlLoWS can prove two types of conformance, named Feeble and Strong conformance (see publication PPDP 2006). The two types of proof are distinguished by means of the option (see options) allow_events_not_expected


help

To get help, type help(topic) at the SICStus prompt. The available topics (links) are represented between stars, as in the following example:

options

Note that topics names are case-sensitive.

To access the developer's manual, type either devman. or devman(topics). at the SCIFF prompt, or read devman.html from the documentation.