Index of values


A
add [Promela.Model]
add m p adds the process p to the model m.
add [Promela.Declarations]
add id t m returns a map containing all bindings of m plus id to t.
add_globals [Promela.Model]
add_globals decls m will return a new model the the global declarations being a union of decls and the previous globals
atomic_section_model [Promela.Normalization]
Rewrite atomic sections to remove superfluous atomic sections on a model
atomic_section_process [Promela.Normalization]
Rewrite atomic sections to remove superfluous atomic sections on a process

B
body_of [Promela.Process]
body_to [Promela.Process]

C
create [Promela.Model]
create a model from a list of processes and global declarations
create [Promela.Process]
create id stmts creates a Promela process named id with a body of stmts; if locals and globals are omitted, the process will not declare local or global variables itself.
create [Promela.Label]
Create a Promela label from an optional attribute and a Promela identifer
create [Promela.Identifier]
Create a Promela identifier from a string; if the lexical convention is violated, Invalid is raised

E
empty [Promela.Model]
create an empty model
empty [Promela.Declarations]
create an empty container of declarations
eval [Promela.Expression]
eval expr tries to evaluate the expression expr as far as possible, thus returning a potentially simpler expression

F
filter [Promela.Model]
filter all statements in the model
filter [Promela.Process]
filter all statements in the process
filter [Promela.Statement]
filter [Promela.Declarations]
find [Promela.Declarations]
fold [Promela.Declarations]

G
globals [Promela.Model]
globals decls m will return a new model with the global declarations being decls
globals_of [Promela.Model]
globals_of m will return the set of global declarations of the model m.

I
id_of [Promela.Process]
identifiers_of [Promela.Statement]
generate a set of all identifiers occuring in a Promela statement
identifiers_of [Promela.Expression]
identifiers_of expr generates a set of all variables occuring in expr
identifiers_of_lst [Promela.Statement]
generate a set of all identifiers occuring in a list of Promela statements
identifiers_read [Promela.Model]
generate a set of all identifiers that are read by the model
identifiers_read [Promela.Process]
generate a set of all identifiers that are read by the process
identifiers_read [Promela.Statement]
generate a set of all identifiers that are read by a Promela statement.
identifiers_written [Promela.Model]
generate a set of all identifiers that are written by the model
identifiers_written [Promela.Process]
generate a set of all identifiers that are written by a process
identifiers_written [Promela.Statement]
generate a set of all identifiers that are written by Promela statement
is_active [Promela.Process]
is_end [Promela.Label]
is_never [Promela.Process]

L
load [Promela.Model]
load ci will load a binary representation of a model from the channel ci.
locals [Promela.Process]
locals decls p will return a new process with the local declarations being decls
locals_of [Promela.Process]
locals_of p will return the set of local declarations of the process p.

M
map [Promela.Process]
map all statements in a process
map [Promela.Statement]
map [Promela.Declarations]
map_rhs [Promela.Model]
map_rhs f m will apply the function f to all right-hand-side expressions of the model m.
map_rhs [Promela.Process]
map_rhs f p will apply the function f to all right-hand-side expressions of the process p.
map_rhs [Promela.Statement]
map_rhs f stmt will apply the function f to all right-hand-side expressions in the statement stmt.
map_stmt [Promela.Model]
map over all statements of the model
mem [Promela.Declarations]
mem id decls is a predicate if there is a declaration for the id id in the declaration container decls

N
never [Promela.Process]

P
processes_of [Promela.Model]
returns the list of processes of the model

R
remove [Promela.Declarations]
remove id decls creates a new declaration map without id
rename [Promela.Declarations]
Rename all declarations of a set by applying a renaming function to them
rename_variables [Promela.Model]
rename_variables f m applies the renaming function f to all identifiers occuring in the model m.
rename_variables [Promela.Process]
rename_variables f p applies the renaming function f to all identifiers occuring in the process p.
rename_variables [Promela.Statement]
rename_variables f stmt applies the renaming function f to all identifiers occuring in stmt
rename_variables [Promela.Expression]
rename_variables f expr applies the renaming function f to all variables in expr
rename_variables_lst [Promela.Statement]
rename_variables f stmts applies the renaming function f to all identifiers occuring in the list stmts

S
save [Promela.Model]
save co m will generate a binary representation of the model m and write it to channel co.
size [Promela.Model]
size m computes the state-vector size of the model m in bit
size [Promela.Type]
size t returns the size of the type t in bit
string_of [Promela.Statement]
generate valid Promela code from a Promela statement
string_of [Promela.Declarations]
generate a string in valid Promela of all declarations in a set
string_of [Promela.Expression]
Get the Promela-compatible string representation of the expression
string_of [Promela.Type]
Get the string representation of the type
string_of [Promela.Label]
Get the string representation of the label; this is the same as the Promela identifier including an optional prefix depending on the applied attribute
string_of [Promela.Identifier]
Get the Promela identifier as a string
string_of_lst [Promela.Statement]
generate valid Promela code from a list of Promela statements

T
to_channel [Promela.Model]
to_channel co m writes valid Promela code for the given model m to channel co.
to_channel [Promela.Process]
to_channel co p writes valid Promela code for the given process p to channel co.
to_channel [Promela.Statement]
write valid Promela code for a Promela statement to a file, indenting it by ident spaces
to_channel [Promela.Declarations]
write all declarations as valid Promlea to a file
to_channel_lst [Promela.Statement]
write valid Promela code for a list of Promela statements to a file, indenting it by ident spaces

U
union [Promela.Model]
union m1 m2 generates a new model including all processes if m1 and m2 and the union of the global declarations of m1 and m2.
union [Promela.Declarations]