Module Import

module Import: sig  end

Importation of an EVA specification in abstract syntax (multi-process) into a list of clauses

val horn_instr : Clause.state -> string -> Abstract.eva_instr -> Clause.clause list

horn_instr st lab i
Returns a list of horn clauses computed with:

the state st (current state),
the string lab (next label),
the instruction i

The clause are, for the following instructions:

SEND t: st => st', st' => KNOWS t (where st' is the principal's state successor of st).
RECV t: st, KNOWS t => st'

val horn_linstr : Clause.state -> string -> Abstract.eva_linstr -> Clause.clause list

horn_linstr st lab i
Returns a list of horn clauses computed with:

the state st (current state),
the string lab (next label),
the located instruction i

val horn_linstrlist : Clause.state -> Abstract.eva_linstr list -> Clause.clause list

horn_linstrlist st il
Returns a list of transition clauses starting at state st and following the located instruction list il.

val horn_process : Clause.state -> Abstract.eva_process -> Clause.clause list

horn_process init_state pr
Returns the clause list built from the given initial state init_state and the given program pr.pr_messages.

val horn_lprotocol : Clause.state list -> Abstract.eva_lprotocol -> Clause.clause list

horn_protocol sl pr
Returns the clause list built from the given located protocol pr and the given list of initial states sl.

val horn_lsession : Clause.state list ->
       Symbols.eva_symbol_list -> Abstract.eva_lsession -> Clause.clause list

horn_session stl sl s
Returns a list of clauses defining an initial subdomain according to the given located session declaration s and the given list of initial states stl, and the given symbol list sl (for horn_bang).

val horn_assume_lstatement : Abstract.eva_lstatement -> Clause.clause list

val horn_claim_lstatement : string list ->
       Clause.state list -> Abstract.eva_lstatement -> Clause.clause list

horn_claim_lstatement rl stl f
Returns the list of clauses associated to the given claim located statement f, given a role list rl and a set of states stl.

val horn_spec : Symbols.eva_symbol_list -> Abstract.eva_spec -> Clause.tclause list

horn_spec sp
Returns the list of clauses corresponding to the given spec sp.