Module ContinuousRule

module ContinuousRule: sig .. end

Structure rewriting with continuous dynamics.

Basic Type Definition

type rule = {

`discrete :DiscreteRule.rule;`	`(*`	The discrete part	`*)`
`dynamics :Formula.eq_sys;`	`(*`	Equation system calD	`*)`
`update :Formula.eq_sys;`	`(*`	Update equations calT	`*)`
`inv :Formula.formula;`	`(*`	Invariant for the evolution	`*)`
`post :Formula.formula;`	`(*`	Postcondition for application	`*)`

}

Specification of a continuous rewriting rule, as in modelling document. Function named foo on element i is, in a term, given by variable foo_i.

val make_rule : (string * (string list * Formula.formula)) list ->
       DiscreteRule.rule ->
       Formula.eq_sys ->
       Formula.eq_sys ->
       ?inv:Formula.formula -> ?post:Formula.formula -> unit -> rule

Create a continuous rule given a named discrete rule and other params.

Printing function

val str : rule -> string

Print a rule to string.

val fprint_full : bool -> Format.formatter -> rule -> unit

val fprint : Format.formatter -> rule -> unit

val print : rule -> unit

val sprint : rule -> string

val matching_str : Structure.structure -> (string * int) list -> string

Applying function to side structures

val apply_to_side : bool ->
       (Structure.structure -> Structure.structure * 'a) ->
       (string * int) list ->
       (string * (string list * Formula.formula)) list ->
       rule -> rule

Apply f to left (if to_left) or right side of the given rule. Return the new rule and an additional result which f returns.

val lhs : rule -> Structure.structure option

val rhs : rule -> Structure.structure option

val map_to_formulas : (Formula.formula -> Formula.formula) ->
       rule -> rule

val fold_over_formulas : (Formula.formula -> 'a -> 'a) -> rule -> 'a -> 'a

Finding applicable matches

val matches : Structure.structure -> rule -> DiscreteRule.matching list

Find all matches of r in struc which satisfy r's precondition.

val matches_post : Structure.structure ->
       rule list ->
       rule -> float -> DiscreteRule.matching list

Matches which satisfy postcondition with time 1 and empty params

Rewriting

val rewrite_single_nocheck : Structure.structure ->
       rule list ->
       float ->
       DiscreteRule.matching ->
       rule ->
       float ->
       (string * float) list ->
       Structure.structure * float * ((string * string) * float list) list

For now, we rewrite only single rules, but with universal univs. rewrite_single struc univs cur_time m r t params def_rels rewrites struc for the period t (unless invariant stops holding earlier) starting in cur_time, at matching m, and returns the rewritten structure, the time after the rewrite, and shifts (i.e. values for functions supplied with dynamics equations, at each time step).

val rewrite_single : Structure.structure ->
       rule list ->
       float ->
       DiscreteRule.matching ->
       rule ->
       float ->
       (string * float) list ->
       (Structure.structure * float * ((string * string) * float list) list) option

For now, we rewrite only single rules. Same as ContinuousRule.rewrite_single_nocheck, but check if the postcondition holds. Returns None if rewriting fails.

val compare_diff : ?cmp_funs:(float -> float -> bool) ->
       rule -> rule -> bool * string

Compare two rules and explain the first difference met. Formulas and expressions are compared for structural equality.