Revision 1eda3e78
Added by Xavier Thirioux almost 8 years ago
| src/normalization.ml | ||
|---|---|---|
| 349 | 349 |
List.for_all ((!=) v) inputs_outputs in |
| 350 | 350 |
let orig_vars = inputs_outputs@node.node_locals in |
| 351 | 351 |
let defs, vars = |
| 352 |
List.fold_left (normalize_eq node) ([], orig_vars) node.node_eqs in
|
|
| 352 |
List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
|
|
| 353 | 353 |
(* Normalize the asserts *) |
| 354 | 354 |
let vars, assert_defs, asserts = |
| 355 | 355 |
List.fold_left ( |
| ... | ... | |
| 391 | 391 |
let node = |
| 392 | 392 |
{ node with
|
| 393 | 393 |
node_locals = new_locals; |
| 394 |
node_eqs = defs @ assert_defs;
|
|
| 394 |
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
|
|
| 395 | 395 |
node_asserts = asserts; |
| 396 | 396 |
node_annot = norm_traceability::node.node_annot; |
| 397 | 397 |
} |
Also available in: Unified diff
- work in progress for automata...