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

su4sml/src/wfcpog/liskov_constraint.sml

@@ -198,12 +198,17 @@ fun conjugate_invariants_help [] model = []
     let
 	(* get the invariants of all parents *)
         val parents_and_self = (parents_of class model)@[class]
- 	val invs = List.map (fn a => Predicate(Variable(varcounter.nextStr(),Rep_Core.type_of a),Rep_Core.type_of a,name_of_inv a,[])) parents_and_self
+ 	val invs = List.map (fn a => 
+				let
+				    val term = Predicate(Variable(varcounter.nextStr(),Rep_Core.type_of a),Rep_Core.type_of a,name_of_inv a,[])
+				in
+				    Rep_HolOcl_Helper.holocl_localValid_state term "\\<tau>"
+				end) parents_and_self
     in
 	if (List.length(invs) = 0)
 	then (conjugate_invariants_help clist model)
 	else (["po_lsk_inv"]@["_"]@(name_of class)@["_"],
-	                               conjugate_terms invs)::(conjugate_invariants_help clist model)
+	                               Rep_HolOcl_Helper.holocl_and_all invs)::(conjugate_invariants_help clist model)
 	    
     end
 

su4sml/src/wfcpog/load_model.sml

@@ -61,6 +61,10 @@ val ocl="../../../examples/royals_and_loyals/royals_and_loyals.ocl"
 val remP = []
 *)
 
+(** COMPANY **)
+val zargo = prefix^"company/company.zargo"
+val ocl =""
+val remP =[]
 
 (** SIMPLE **)
 (*
@@ -82,15 +86,18 @@ val ocl = "../../../examples/vehicles/vehicles.ocl"
 *)
 
 (** OVERRRIDING **)
-(*
+(* 
 val zargo = "../../../hol-ocl/examples/overriding/overriding.zargo"
 val ocl="../../../hol-ocl/examples/overriding/overriding.ocl"
 val remP = []
 *)
 
+(** STACK MANU **)
+(* 
 val zargo = prefix^"stack_manu/stack.zargo"
 val ocl=prefix^"stack_manu/stack.ocl"
 val remP = []
+*)
 
 (** import model *)
 val XMI = parseUML zargo

su4sml/src/wfcpog/operational_consistency.sml

@@ -70,7 +70,6 @@ fun impl_op_operation class oper =
 	(* Generate Variables : (sigma_pre,sigma_post) => sigma *)
 	val sigma = Literal("sigma",OclState)
 	val sigma_s = Literal("sigma_s",OclState)
-	val tuple_type = TupleType ([("sigma",OclState),("sigma_s",OclState)])
 	val tuple_term = Tuple [("sigma",sigma,OclState),("sigma_s",sigma_s,OclState)]
 	(* local valid post *)
 	val pre_of_op = Predicate(Variable("self",type_of class),type_of class,name_of_pre class oper,args2varargs (arguments_of_op oper))

su4sml/src/wfcpog/rep_holocl.sml

@@ -241,7 +241,8 @@ sig
     val holocl_implies    : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
     val holocl_not        : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm 
     val holocl_xor        : Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm -> Rep_OclTerm.OclTerm
-
+    val holocl_localValid_state      : Rep_OclTerm.OclTerm -> string -> Rep_OclTerm.OclTerm
+    val holocl_localValid_transition : Rep_OclTerm.OclTerm -> string -> string -> Rep_OclTerm.OclTerm
 end
 structure Rep_HolOcl_Helper:REP_HOLOCL_HELPER = 
 struct 
@@ -270,5 +271,15 @@ fun holocl_implies a b    = ocl_opcall a ["holOclLib","Boolean","implies"] [b] B
 fun holocl_xor a b        = ocl_opcall a ["holOclLib","Boolean","xor"]     [b] Boolean
 fun holocl_not a          = ocl_opcall a ["holOclLib","Boolean","not"]     []  Boolean
 
+fun holocl_localValid_state term var_name = 
+    OperationCall(term,Boolean,["holOclLib","Boolean","OclLocalValid"],[(Literal(var_name,OclState),DummyT)],Boolean)
 
+fun holocl_localValid_transition term var_name1 var_name2 = 
+    let
+	val sigma = Literal(var_name1,OclState)
+	val sigma_s = Literal(var_name2,OclState)
+	val tuple_term = Tuple [(var_name1,sigma,OclState),(var_name2,sigma_s,OclState)]
+    in
+	OperationCall(term,Boolean,["holOclLib","Boolean","OclLocalValid"],[(tuple_term,OclState)],Boolean)
+    end
 end

su4sml/src/wfcpog/test-suite.sml

@@ -204,7 +204,8 @@ fun test (tc:testcase) wfs pos =
     let 
 	val i_model = ModelImport.import (#uml tc) (#ocl tc) []
 	val (clist,alist) = Rep_Core.normalize_ext i_model
-	val model = (((#1 i_model)@oclLib),(#2 i_model))
+(* 	val model = (((#1 i_model)@oclLib),(#2 i_model)) *)
+	val model = ((clist@oclLib),alist)
 	val _ = trace wgen ("Model of testcase loaded ...\n")
 	val x = start_tests model (wfs@pos)
 	val _ = trace wgen ("Test finished ...\n")

su4sml/src/wfcpog/visibility_consistency.sml

@@ -173,8 +173,9 @@ fun check_entity_classifier class model =
     let
 	val vis_ops = List.map (fn (a:operation) => ((#visibility a),SOME(a),NONE,NONE)) (all_operations_of class model)
 	val vis_atts = List.map (fn (a:attribute) => ((#visibility a),NONE,SOME(a),NONE)) (all_attributes_of class model)
-        val vis_assocs = List.map (fn (a:associationend) => ((#visibility a),NONE,NONE,SOME(a))) (all_associationends_of class model)
+(*        val vis_assocs = List.map (fn (a:associationend) => ((#visibility a),NONE,NONE,SOME(a))) (all_associationends_of class model)
 			 handle Bind => raise WFCPOG.WFCPOG_Exception ("Bind exception\n")
+*)
 	val vis_class = visibility_of class
 	val check = 
 	    List.map (fn ((a:Visibility),x,y,z) =>