To get help, type help(topic) at the SICStus prompt. To get help on help, type help(help).
Help available on the following topics:
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.'
In order to create a new project:
mkdir ..\myprj
(Windows syntax)
copy project.pl ..\myprj
ics_file/1,
history_file/1, sokb_file/1
.
The facts ics_file/1,
history_file/1, sokb_file/1
can contain either the path to a file,
or the URL of the file; in the second case, SCIFF will download the file from
the web. The URL should be given as an atomic term, i.e., with single quotes ’,
and should begin with ’http:’. E.g.,
ics_file(’http://lia.deis.unibo.it/Research/sciff/ic.ruleml’).
required_option/2
(see options).
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/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/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/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
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
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('../').
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 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 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.
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.
Print on screen debug messages.
Usually is off.
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.
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.
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.
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.
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.
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
You can inspect the state of an option using the predicate: sciff_option(?Option, ?State).
See also set_option
The predicate show_options shows all the options available and their state
See also get_option, set_option
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
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
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.
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.
The SOKB is a set of clauses, a la logic programming. Each clause is an implication
head :- body.
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:
e(Event,Time)
is a positive expectation
note(Event,Time)
is a negated positive expectation (i.e., the default
negation of a positive expectation)
en(Event,Time)
is a negative expectation
noten(Event,Time)
is a negated negative expectation (the default
negation of en)
abd(Term,Time)
is a general abductive atom
The SOKB can be defined in one or more files.
Each sokb file should be declared in the project.pl
in a fact
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.
Currently, the set of CLP constraints that are interpreted in the ics is the following:
as well as unification = and dis-unification !=
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
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 (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
testing/1
. E.g., add to the SOKB testing(ws).
In AlLoWS, expectations are only positive (E) and have the following syntax:
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/1
will fail in case
the web service is not conformant
allows/1
will succeed
in all cases, useful to inspect the constraint store and have more information
about the history that proves non compliance
allows/1
prints all the possible histories.
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
To get help, type help(topic) at the SICStus prompt. The available topics (links) are represented between stars, as in the following example:
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.