ipg-template.dfy

/*INV{
{
# text at the begining of the file
prelude : """
"""

module_name : module_name

# text at the beginning of the module definition
module_prelude : """
"""

# if you have template arguments
template_args : "<I>"

state_name : s, state_type_name : State
shadow_name : a, shadow_type_name : Aux

operations : [ Op1 Op2 ]

properties :
# begin of properties
[
}INV*/

/*INV{
# end of properties
]
module_postlude : """
"""
}
}INV*/