HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7824 3260e6d1-4efc-4170-b0a7-36055960796d

This commit is contained in:
Manuel Krucker 2008-04-30 08:21:42 +00:00
parent 92d3cdcfcb
commit 876fc95e44
2 changed files with 16 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
su4sml/src/wfcpog/data_model_consistency.sml
View File

@ -119,7 +119,7 @@ fun strong_model_consistency_help classes model =
val _ = trace function_calls("WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency\n")
val terms = List.map (c_allInstance_term) classes
val local_valids = List.map (fn a => OperationCall(a,Boolean,["holOclLib","Boolean","OclLocalValid"],[(Literal("\\<tau>",OclState),DummyT)],Boolean)) terms
val con_term = conjugate_terms local_valids
val con_term = conjugate_holoclterms local_valids
val dummy_source = Literal("",DummyT)
val res = Iterator("holOclLib.exists",[("\\<tau>",OclState)],dummy_source,DummyT,con_term,Boolean,Boolean)
val _ = trace function_ends("WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency\n")

17
su4sml/src/wfcpog/library.sml
View File

@ -57,9 +57,11 @@ sig
val term_of_postcondition : (string option * Rep_OclTerm.OclTerm) -> Rep_OclTerm.OclTerm
(** Wrap a predicate over an OclTerm.*)
(* val wrap_predicate : Rep_OclTerm.OclTerm -> string option -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list -> Rep_OclTerm.OclTerm *)
(** Conjugate a list of terms to one single term.*)
(** Conjungtion of a list of OclTerms to one single term.*)
val conjugate_terms : Rep_OclTerm.OclTerm list -> Rep_OclTerm.OclTerm
(** *)
(** Conjungtion of a list of HolOclTerms to one single term.*)
val conjugate_holoclterms : Rep_OclTerm.OclTerm list -> Rep_OclTerm.OclTerm
(** Disjunction of a list of OclTerms to one single term.*)
val disjugate_terms : Rep_OclTerm.OclTerm list -> Rep_OclTerm.OclTerm
(** Get an attribute by name. *)
val get_attribute : string -> Rep_Core.Classifier -> Rep.Model -> Rep_Core.attribute
@ -126,6 +128,17 @@ fun conjugate_terms [] = raise WFCPOG_LibraryError ("Empty list not conjugateabl
else raise WFCPOG_LibraryError ("type of term is not Boolean. \n")
end
fun conjugate_holoclterms [] = raise WFCPOG_LibraryError ("Empty list not conjugateable. \n")
| conjugate_holoclterms [x] = x
| conjugate_holoclterms (h::tail) =
let
val x = conjugate_holoclterms tail
in
if (type_of_term h = Boolean)
then (OperationCall(h,type_of_term h,["holOclLib","Boolean","and"],[(x,type_of_term x)],Boolean))
else raise WFCPOG_LibraryError ("type of term is not Boolean. \n")
end
fun disjugate_terms [] = raise WFCPOG_LibraryError("Empty list not disjugateable. \n")
| disjugate_terms [x:OclTerm] = (x)
| disjugate_terms ((h:OclTerm)::tail) =