From 49bdc228540187e6d012f52785274d6bdf05fca9 Mon Sep 17 00:00:00 2001 From: Manuel Krucker Date: Wed, 2 Apr 2008 11:37:27 +0000 Subject: [PATCH] git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7577 3260e6d1-4efc-4170-b0a7-36055960796d --- su4sml/src/wfcpo-gen/refine_constraint.sml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/su4sml/src/wfcpo-gen/refine_constraint.sml b/su4sml/src/wfcpo-gen/refine_constraint.sml index 94e20bc..7262ce7 100644 --- a/su4sml/src/wfcpo-gen/refine_constraint.sml +++ b/su4sml/src/wfcpo-gen/refine_constraint.sml @@ -275,7 +275,9 @@ fun get_holocl_abstraction_relation abs_package conc_package model = fun get_holocl_invariant class model = let val _ = trace function_calls ("WFCPOG_Refine_Constraint.get_holocl_invariant\n") - val res = Predicate(Variable("x",typ),typ,hol_name,args) + val hol_name = mk_def_of (name_of class) + val typ = type_of class + val res = Predicate(Variable("x",typ),typ,hol_name,[]) val _ = trace function_ends ("WFCPOG_Refine_Constraint.get_holocl_invariant\n") in res @@ -305,7 +307,7 @@ fun pre_state_valid hol_operation ((Tuple(tuple)):OclTerm) V = (* (string * term * type) *) val (sigma'_name,sigma'_term,sigma'_type) = List.last tuple (* sigma is_element_of V *) - val s_E_V = Predicate(V,DummyT, +(* val s_E_V = Predicate(V,DummyT, *) val m_valid = M_valid hol_operation (Tuple(tuple)) val exists = Iterator("holOclLib.exists",[(sigma'_name,sigma'_type)],V,Boolean,m_valid,Boolean,Boolean) val res = Iterator("holOclLib.forAll",[(sigma_name,sigma_type)],V,Boolean,exists,Boolean,Boolean)