From 33a6f501a8fbc038bc1c385705ba92db73c62b45 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 25 Mar 2009 17:13:38 +0000 Subject: [PATCH] trace is now Logger git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@8438 3260e6d1-4efc-4170-b0a7-36055960796d --- su4sml/src/ROOT.ML | 1 + su4sml/src/wfcpog/SecureUML_constraint.sml | 27 ++-- .../src/wfcpog/command_query_consistency.sml | 11 +- su4sml/src/wfcpog/constructor_consistency.sml | 33 ++--- su4sml/src/wfcpog/data_model_consistency.sml | 15 +-- su4sml/src/wfcpog/datatab.sml | 2 +- su4sml/src/wfcpog/interface_consistency.sml | 11 +- su4sml/src/wfcpog/library.sml | 9 +- su4sml/src/wfcpog/liskov_constraint.sml | 3 +- su4sml/src/wfcpog/operational_consistency.sml | 15 +-- su4sml/src/wfcpog/refine_constraint.sml | 119 +++++++++--------- su4sml/src/wfcpog/rep_holocl.sml | 11 +- su4sml/src/wfcpog/taxonomy_consistency.sml | 9 +- su4sml/src/wfcpog/test-data.sml | 26 ++-- su4sml/src/wfcpog/test-suite.sml | 32 ++--- su4sml/src/wfcpog/visibility_consistency.sml | 41 +++--- su4sml/src/wfcpog/wfcpog.sml | 2 +- su4sml/src/wfcpog/wfcpog_registry.sml | 24 ++-- 18 files changed, 201 insertions(+), 190 deletions(-) diff --git a/su4sml/src/ROOT.ML b/su4sml/src/ROOT.ML index c95c14b..90aa438 100644 --- a/su4sml/src/ROOT.ML +++ b/su4sml/src/ROOT.ML @@ -114,6 +114,7 @@ use "ocl2dresdenjava.sml"; (* ****************************************************** *) (* Main Conversion Processes *) +use "config.sml"; use "xmltree.sml"; use "xmltree_helper.sml"; use "xmltree_hooks.sml"; diff --git a/su4sml/src/wfcpog/SecureUML_constraint.sml b/su4sml/src/wfcpog/SecureUML_constraint.sml index 92974d7..1582162 100644 --- a/su4sml/src/wfcpog/SecureUML_constraint.sml +++ b/su4sml/src/wfcpog/SecureUML_constraint.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -103,10 +104,10 @@ fun ssd_generate_pos [] classes model = [] fun separation_of_duty_help [] classes model = []:((Path * OclTerm) list ) | separation_of_duty_help (h::perm_sets) classes model = let - val _ = trace function_calls ("WFCPOG_SecureUML_Constraint.separation_of_duty_help\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.separation_of_duty_help\n") val x = ssd_generate_pos h classes model val res = x@(separation_of_duty_help perm_sets classes model) - val _ = trace function_calls ("WFCPOG_SecureUML_Constraint.separation_of_duty_help\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.separation_of_duty_help\n") in res end @@ -118,39 +119,39 @@ fun binding_of_duty_help [] (cl::clist) model = [] (* fun rh_is_tree wfpo (model as (clist,alist)) = let - val _ = trace funciton_calls ("WFCPOG_SecureUML_Constraint.rh_is_tree\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.rh_is_tree\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Role a)) cl - val _ = trace funciton_calls ("WFCPOG_SecureUML_Constraint.rh_is_tree\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.rh_is_tree\n") in res end *) fun separation_of_duty wfpo (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_SecureUML_Constraint.separation_of_duty\n") - val _ = trace wgen ("remove OclLib ...\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.separation_of_duty\n") + val _ = Logger.debug1 ("remove OclLib ...\n") val cl = removeOclLibrary clist - val _ = trace wgen ("oclLib removed ...\n") - val _ = trace wgen ("Extract args ...\n") + val _ = Logger.debug1 ("oclLib removed ...\n") + val _ = Logger.debug1 ("Extract args ...\n") val ssd_args = WFCPOG_SSD_Data.get wfpo val perm_sets = (#mutex_perm_sets ssd_args) val res = separation_of_duty_help perm_sets cl model - val _ = trace function_ends ("WFCPOG_SecureUML_Constraint.separation_of_duty\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.separation_of_duty\n") in res end fun binding_of_duty wfpo (model as (clist,alist)) = []:((Path * OclTerm) list) (* let - val _ = trace function_calls ("WFCPOG_SecureUML_Constraint.binding_of_duty\n") - val _ = trace wgen ("remove OclLib ...\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.binding_of_duty\n") + val _ = Logger.debug1 ("remove OclLib ...\n") val cl = removeOclLibrary clist val res = binding_of_duty cl model - val _ = trace function_ends ("WFCPOG_SecureUML_Constraint.binding_of_duty\n") + val _ = Logger.info ("WFCPOG_SecureUML_Constraint.binding_of_duty\n") in res end diff --git a/su4sml/src/wfcpog/command_query_consistency.sml b/su4sml/src/wfcpog/command_query_consistency.sml index d158e7b..b630774 100644 --- a/su4sml/src/wfcpog/command_query_consistency.sml +++ b/su4sml/src/wfcpog/command_query_consistency.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -160,11 +161,11 @@ fun check_strong_classifier class (model as (clist,alist)) = fun weak_is_query po (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Command_Query_Constraint.strong_is_query\n") + val _ = Logger.info ("WFCPOG_Command_Query_Constraint.strong_is_query\n") val classes = removeOclLibrary clist val res = List.all (fn a => a = true) (List.map (fn a => check_weak_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException(po,s)) classes) - val _ = trace function_ends ("WFCPOG_Command_Query_Constraint.strong_is_query\n") + val _ = Logger.info ("WFCPOG_Command_Query_Constraint.strong_is_query\n") in res end @@ -173,11 +174,11 @@ fun weak_is_query po (model as (clist,alist)) = fun strong_is_query po (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Command_Query_Constraint.strong_is_query\n") + val _ = Logger.info ("WFCPOG_Command_Query_Constraint.strong_is_query\n") val classes = removeOclLibrary clist val res = List.all (fn a => a = true) (List.map (fn a => check_strong_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException(po,s)) classes) - val _ = trace function_ends ("WFCPOG_Command_Query_Constraint.strong_is_query\n") + val _ = Logger.info ("WFCPOG_Command_Query_Constraint.strong_is_query\n") in res end diff --git a/su4sml/src/wfcpog/constructor_consistency.sml b/su4sml/src/wfcpog/constructor_consistency.sml index 6c48677..ff68a7a 100644 --- a/su4sml/src/wfcpog/constructor_consistency.sml +++ b/su4sml/src/wfcpog/constructor_consistency.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -72,11 +73,11 @@ exception WFCPO_ConstructorError of string fun term_post_implies_inv class oper model = let - val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.term_post_implies_inv\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.term_post_implies_inv\n") val inv = Predicate (Variable("self",type_of class),type_of class,name_of_inv class,[]) val post = Predicate (Variable ("self",type_of class),type_of class,name_of_post class oper,args2varargs ((arguments_of_op oper)@[("result",(#result oper))])) val implies = OperationCall (post,Boolean,["holOclLib","Boolean","implies"],[(inv,Boolean)],Boolean) - val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.term_post_implies_inv\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.term_post_implies_inv\n") in implies end @@ -84,7 +85,7 @@ fun term_post_implies_inv class oper model = fun term_init_attributes class oper model = let val atts = all_attributes_of class model - val _ = trace wgen ("Number of attributes found = "^(Int.toString(List.length(atts)))) + val _ = Logger.debug1 ("Number of attributes found = "^(Int.toString(List.length(atts)))) val post = Predicate (Variable ("self",type_of class),type_of class,name_of_post class oper,args2varargs ((arguments_of_op oper)@[("result",(#result oper))])) val att_is_defined = List.map (fn a => @@ -103,7 +104,7 @@ fun term_init_attributes class oper model = fun check_override_classifier class (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") val creas = creation_operations_of class model val over_ops = modified_operations_of class model val check = @@ -118,14 +119,14 @@ fun check_override_classifier class (model as (clist,alist)) = raise WFCPOG.WFC_FailedMessage (s1^s2) end) creas val res = List.all (fn a => a = true) check - val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") in res end fun generate_post_classifier class model = let - val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.check_post_classifier\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.check_post_classifier\n") val atts = all_attributes_of class model val pos = if (List.length(atts) = 0) then [] @@ -137,7 +138,7 @@ fun generate_post_classifier class model = in (path,term) end) (creation_operations_of class model) - val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") in pos end @@ -145,7 +146,7 @@ fun generate_post_classifier class model = fun generate_attribute_classifier class model = let - val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.generate_attribute_classifier\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.generate_attribute_classifier\n") val pos = List.map (fn a => let @@ -154,7 +155,7 @@ fun generate_attribute_classifier class model = in (path,term) end) (creation_operations_of class model) - val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.generate_attribute_classifier\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.generate_attribute_classifier\n") in pos end @@ -162,23 +163,23 @@ fun generate_attribute_classifier class model = fun override_old_creators wfpo (model as (clist, alist)) = let - val _ = trace function_calls ("WFCPOG_Constructor_Consistency.overrides_old_creators\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency.overrides_old_creators\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl val res = List.all (fn a => a = true) (List.map (fn a => check_override_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s)) classes) - val _ = trace function_calls ("WFCPOG_Constructor_Consistency.overrides_old_creators\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency.overrides_old_creators\n") in res end fun post_implies_invariant wfpo (model as (clist, alist)) = let - val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.post_implies_invariant\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.post_implies_invariant\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl val list = List.concat (List.map (fn a => generate_post_classifier a model) classes) - val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.post_implies_invariant\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.post_implies_invariant\n") in list end @@ -186,11 +187,11 @@ fun post_implies_invariant wfpo (model as (clist, alist)) = fun force_initialize_attributes wfpo (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.force_initialize_attributes\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.force_initialize_attributes\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl val list = List.concat (List.map (fn a => generate_attribute_classifier a model) classes) - val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.force_initialize_attributes\n") + val _ = Logger.info ("WFCPOG_Constructor_Consistency_Constraint.force_initialize_attributes\n") in list end diff --git a/su4sml/src/wfcpog/data_model_consistency.sml b/su4sml/src/wfcpog/data_model_consistency.sml index 2de8f02..8e18b23 100644 --- a/su4sml/src/wfcpog/data_model_consistency.sml +++ b/su4sml/src/wfcpog/data_model_consistency.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -71,7 +72,7 @@ exception WFCPO_DataModelError fun c_allInstance_term (c:Classifier) = let - val _ = trace function_calls ("WF_data_CS.c_allInstances\n") + val _ = Logger.info ("WF_data_CS.c_allInstances\n") val class_type = type_of c val x_name = ("c_"^(varcounter.nextStr())) val x = Variable (x_name,class_type) @@ -84,7 +85,7 @@ fun c_allInstance_term (c:Classifier) = val oclIsTypeOf = OperationWithType (x,DummyT,"oclIsTypeOf",class_type,Boolean) (* Iterator exists *) val exists = Iterator("exists",[(x_name,class_type)],allInstances,Set(class_type),oclIsTypeOf,Boolean,Boolean) - val _ = trace function_ends ("WF_data_CS.c_allInstances\n") + val _ = Logger.info ("WF_data_CS.c_allInstances\n") in exists end @@ -92,12 +93,12 @@ fun c_allInstance_term (c:Classifier) = (* E t. t |= c::allInstances()->exists(x|x.oclIsTypeOf(c)) *) fun single_model_consistency (c:Classifier) (model as (clist,alist)) = let - val _ = trace function_calls("WFCPOG_Data_Model_Consistency_Constraint.single_model_consistency\n") + val _ = Logger.info("WFCPOG_Data_Model_Consistency_Constraint.single_model_consistency\n") val term = c_allInstance_term c val local_valid = OperationCall(term,Boolean,["holOclLib","Boolean","OclLocalValid"],[(Literal("\\",OclState),DummyT)],Boolean) val dummy_source = Literal("",DummyT) val res = Iterator("holOclLib.exists",[("\\",OclState)],dummy_source,DummyT,local_valid,Boolean,Boolean) - val _ = trace function_ends("WFCPOG_Data_Model_Consistency_Constraint.single_model_consistency\n") + val _ = Logger.info("WFCPOG_Data_Model_Consistency_Constraint.single_model_consistency\n") in res end @@ -116,13 +117,13 @@ fun class_model_consistency wfpo (model as (clist,alist)) = fun strong_model_consistency_help classes model = let - val _ = trace function_calls("WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency\n") + val _ = Logger.info("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("\\",OclState),DummyT)],Boolean)) terms val con_term = holocl_and_all local_valids val dummy_source = Literal("",DummyT) val res = Iterator("holOclLib.exists",[("\\",OclState)],dummy_source,DummyT,con_term,Boolean,Boolean) - val _ = trace function_ends("WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency\n") + val _ = Logger.info("WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency\n") in [(["po_strong_model"],res)] end diff --git a/su4sml/src/wfcpog/datatab.sml b/su4sml/src/wfcpog/datatab.sml index b4571e1..0fb6419 100644 --- a/su4sml/src/wfcpog/datatab.sml +++ b/su4sml/src/wfcpog/datatab.sml @@ -5,7 +5,7 @@ * datatab.sml --- a very simplistic datatab implementation * This file is part of su4sml. * - * Copyright (c) 2008 Achim D. Brucker, Germany + * Copyright (c) 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * diff --git a/su4sml/src/wfcpog/interface_consistency.sml b/su4sml/src/wfcpog/interface_consistency.sml index 7de4920..1218a64 100644 --- a/su4sml/src/wfcpog/interface_consistency.sml +++ b/su4sml/src/wfcpog/interface_consistency.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -167,24 +168,24 @@ fun check_nameclash_classifier (c as Class{interfaces,...}) (model as (clist,ali fun check_stereotypes wfpo (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Interface_Consistency.check_stereotypes\n") + val _ = Logger.info ("WFCPOG_Interface_Consistency.check_stereotypes\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Iface a)) cl val res = List.all (fn a => a = true) (List.map (fn a => check_stereotypes_interface a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s)) classes) - val _ = trace function_ends ("WFCPOG_Interface_Consistency.check_stereotypes\n") + val _ = Logger.info ("WFCPOG_Interface_Consistency.check_stereotypes\n") in res end fun check_nameclashes wfpo (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Interface_Consistency.check_nameclashes\n") + val _ = Logger.info ("WFCPOG_Interface_Consistency.check_nameclashes\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a) orelse (is_Primi a) orelse (is_Enum a)) cl val res = List.all (fn a => a = true) (List.map (fn a => check_nameclash_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s)) classes) - val _ = trace function_ends ("WFCPOG_Interface_Consistency.check_nameclashes\n") + val _ = Logger.info ("WFCPOG_Interface_Consistency.check_nameclashes\n") in res diff --git a/su4sml/src/wfcpog/library.sml b/su4sml/src/wfcpog/library.sml index 369077a..62c873f 100644 --- a/su4sml/src/wfcpog/library.sml +++ b/su4sml/src/wfcpog/library.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -206,9 +207,7 @@ fun class_has_local_op name model classifier = fun get_operation s classifier model = let - val _ = trace 100 ("get_operation: \n") val x = List.find (fn a => if (name_of_op a = s) then true else false) (all_operations_of classifier model) - val _ = trace 100 ("end get_operation\n") in case x of NONE => raise WFCPOG_LibraryError ("No operation found using 'get_operation'.\n") @@ -223,7 +222,7 @@ fun get_attribute s classifier model = case x of NONE => let - val _ = trace exce ("No such Attribute: \n In Classifier "^(string_of_path (name_of classifier))^" in attribute "^s) + val _ = Logger.info ("No such Attribute: \n In Classifier "^(string_of_path (name_of classifier))^" in attribute "^s) in raise WFCPOG_LibraryError ("No attribute found using 'get_attribute'.\n") end @@ -237,7 +236,7 @@ fun get_associationend s classifier model = case x of NONE => let - val _ = trace exce ("No such associationend: \n In Classifier "^(string_of_path (Rep_Core.name_of classifier))^" no associationend called "^(s)^".\n") + val _ = Logger.info ("No such associationend: \n In Classifier "^(string_of_path (Rep_Core.name_of classifier))^" no associationend called "^(s)^".\n") in raise WFCPOG_LibraryError ("No attribute found using 'get_attribute'.\n") end diff --git a/su4sml/src/wfcpog/liskov_constraint.sml b/su4sml/src/wfcpog/liskov_constraint.sml index 95996ba..553bfd9 100644 --- a/su4sml/src/wfcpog/liskov_constraint.sml +++ b/su4sml/src/wfcpog/liskov_constraint.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * diff --git a/su4sml/src/wfcpog/operational_consistency.sml b/su4sml/src/wfcpog/operational_consistency.sml index 8c9602d..3bc8467 100644 --- a/su4sml/src/wfcpog/operational_consistency.sml +++ b/su4sml/src/wfcpog/operational_consistency.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -65,7 +66,7 @@ exception WFCPO_OperationalError fun impl_op_operation class oper = let - val _ = trace function_calls ("WFCPOG_Operational_Consistency.prestate_complete_operation\n") + val _ = Logger.info ("WFCPOG_Operational_Consistency.prestate_complete_operation\n") (* Generate Variables : (sigma_pre,sigma_post) => sigma *) val sigma = Literal("sigma",OclState) val sigma_s = Literal("sigma_s",OclState) @@ -78,27 +79,27 @@ fun impl_op_operation class oper = val lv_state = OperationCall(impl,Boolean,["holOclLib","Boolean","OclLocalValid"],[(tuple_term,OclState)],Boolean) val holocl_exists = Iterator("holOclLib.exists",[("sigma_s",OclState)],Literal("",DummyT),DummyT,lv_state,Boolean,Boolean) val holocl_forall = Iterator("holOclLib.forAll",[("sigma",OclState)],Literal("",DummyT),DummyT,holocl_exists,Boolean,Boolean) - val _ = trace function_ends ("WFCPOG_Operational_Consistency.prestate_complete_operaiton\n") + val _ = Logger.info ("WFCPOG_Operational_Consistency.prestate_complete_operaiton\n") in holocl_forall end fun impl_op_classifier class (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Operational_Consistency.prestate_complete_classifier\n") + val _ = Logger.info ("WFCPOG_Operational_Consistency.prestate_complete_classifier\n") val ops = all_operations_of class model val res = (List.map (fn a => ((["po_class_model_"]@(name_of class)@["_"]@[(name_of_op a)]),(impl_op_operation class a))) ops) - val _ = trace function_ends ("WFCPOG_Operational_Consistency.prestate_complete_classifier\n") + val _ = Logger.info ("WFCPOG_Operational_Consistency.prestate_complete_classifier\n") in res end fun implementable_operation wfc_sel (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Operational_Consistency.prestate_complete\n") + val _ = Logger.info ("WFCPOG_Operational_Consistency.prestate_complete\n") val cl = removeOclLibrary clist val res = List.concat (List.map (fn a => impl_op_classifier a model) cl ) - val _ = trace function_ends ("WFCPOG_Operational_Consistency.prestate_complete\n") + val _ = Logger.info ("WFCPOG_Operational_Consistency.prestate_complete\n") in res end diff --git a/su4sml/src/wfcpog/refine_constraint.sml b/su4sml/src/wfcpog/refine_constraint.sml index e215ec9..5075a67 100644 --- a/su4sml/src/wfcpog/refine_constraint.sml +++ b/su4sml/src/wfcpog/refine_constraint.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -111,8 +112,8 @@ fun group_cl [] [] = [] end | group_cl (h1::t1) list = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.group_cl \n") - val _ = trace wgen ("Class: " ^ string_of_path (name_of h1) ^ "\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.group_cl \n") + val _ = Logger.debug1 ("Class: " ^ string_of_path (name_of h1) ^ "\n") val x = List.filter (fn a => ((List.last (name_of a)) = (List.last (name_of h1)))) list val res = case (List.length(x)) of @@ -131,7 +132,7 @@ fun group_cl [] [] = [] in raise WFCPOG.WFC_FailedMessage (s1^s2) end - val _ = trace function_ends ("WFCPOG_Refine_Constraint.group_cl \n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.group_cl \n") in res end @@ -148,7 +149,7 @@ fun group_op class_name [] [] = [] | group_op class_name ((h1:operation)::t1) list = let (* TODO: Check also signature because of the overloaded operations! *) - val _ = trace function_calls ("WFCPOG_Refine_Constraint.group_op \n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.group_op \n") val x = (List.filter (fn a => ((name_of_op a) = (name_of_op h1))) list) val res = case (List.length(x)) of @@ -167,7 +168,7 @@ fun group_op class_name [] [] = [] in raise WFCPOG.WFC_FailedMessage (s1^s2) end - val _ = trace function_ends ("WFCPOG_Refine_Constraint.group_op \n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.group_op \n") in res end @@ -175,17 +176,17 @@ fun group_op class_name [] [] = [] (* RETURN: (Classifier * Classifer) list *) fun map_public_classes fromPath toPath (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.map_public_classes\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.map_public_classes\n") val abs_c = List.filter (is_visible_cl) (List.filter (fn a => if (package_of a = fromPath) then true else false) (clist)) - val _ = trace wgen ("abstract public classes: \n") - val _ = List.map (fn a => trace wgen (" - " ^ (string_of_path (name_of a))^"\n")) abs_c - val _ = trace wgen ("map_public_classes 2 \n") - val _ = trace wgen ("Package " ^ string_of_path (fromPath) ^ " contains " ^ Int.toString (List.length(abs_c)) ^ " public classes.\n") + val _ = Logger.debug1 ("abstract public classes: \n") + val _ = List.map (fn a => Logger.debug1 (" - " ^ (string_of_path (name_of a))^"\n")) abs_c + val _ = Logger.debug1 ("map_public_classes 2 \n") + val _ = Logger.debug1 ("Package " ^ string_of_path (fromPath) ^ " contains " ^ Int.toString (List.length(abs_c)) ^ " public classes.\n") val conc_c = List.filter (is_visible_cl) (List.filter (fn a => if (package_of a = toPath) then true else false) (clist)) - val _ = trace wgen ("concrete public classes: \n") - val _ = List.map (fn a => trace wgen (" - " ^ (string_of_path (name_of a))^"\n")) conc_c - val _ = trace wgen ("Package " ^ string_of_path (toPath) ^ " contains " ^ Int.toString (List.length(conc_c)) ^ " public classes.\n") - val _ = trace wgen ("map_public_classes 3 \n") + val _ = Logger.debug1 ("concrete public classes: \n") + val _ = List.map (fn a => Logger.debug1 (" - " ^ (string_of_path (name_of a))^"\n")) conc_c + val _ = Logger.debug1 ("Package " ^ string_of_path (toPath) ^ " contains " ^ Int.toString (List.length(conc_c)) ^ " public classes.\n") + val _ = Logger.debug1 ("map_public_classes 3 \n") val res = group_cl abs_c conc_c (* handle WFCPOG.WFC_FailedMessage s => @@ -196,7 +197,7 @@ fun map_public_classes fromPath toPath (model as (clist,alist)) = in raise WFCPOG.WFC_FailedMessage (s1^s2^s3) end - val _ = trace function_calls ("WFCPOG_Refine_Constraint.map_public_classes\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.map_public_classes\n") *) in res @@ -205,11 +206,11 @@ fun map_public_classes fromPath toPath (model as (clist,alist)) = fun map_public_ops [] = [[]] | map_public_ops ((f,t)::tail) = let - val _ = trace function_calls ("Refine_Constraint.map_public_ops\n") + val _ = Logger.info ("Refine_Constraint.map_public_ops\n") val f_ops = List.filter (is_visible_op) (local_operations_of f) val t_ops = List.filter (is_visible_op) (local_operations_of t) - val _ = trace wgen ("Number of operations of f_class(" ^ (string_of_path (name_of f)) ^ ") = " ^ Int.toString (List.length(f_ops)) ^ "\n") - val _ = trace wgen ("Number of operations of t_class(" ^ (string_of_path (name_of t)) ^ ") = " ^ Int.toString (List.length(t_ops)) ^ "\n") + val _ = Logger.debug1 ("Number of operations of f_class(" ^ (string_of_path (name_of f)) ^ ") = " ^ Int.toString (List.length(f_ops)) ^ "\n") + val _ = Logger.debug1 ("Number of operations of t_class(" ^ (string_of_path (name_of t)) ^ ") = " ^ Int.toString (List.length(t_ops)) ^ "\n") val res = [(List.map (fn (a,b) => (f,t,a,b)) (group_op (List.last (Rep_Core.name_of f)) f_ops t_ops handle OpGroupError (oplist,s) => @@ -224,7 +225,7 @@ fun map_public_ops [] = [[]] end ))] @(map_public_ops tail) - val _ = trace function_ends ("Refine_Constraint.map_public_op\n") + val _ = Logger.info ("Refine_Constraint.map_public_op\n") in res end @@ -234,23 +235,23 @@ fun map_public_ops [] = [[]] fun map_types [] fP tP model = [] | map_types ((h1:Classifier,h2:Classifier,h3:operation,h4:operation)::tail) fP tP model = let - val _ = trace function_calls ("WFCPOG_Refine_Constrain.map_types\n") - val _ = trace wgen ("map_types: f_cl = " ^ string_of_path (name_of h1) ^ "\n") - val _ = trace wgen ("map_types: t_cl = " ^ string_of_path (name_of h2) ^ "\n") - val _ = trace wgen ("map_types: f_op = " ^ name_of_op h3 ^ "\n") - val _ = trace wgen ("map_types: t_op = " ^ name_of_op h4 ^ "\n") + val _ = Logger.info ("WFCPOG_Refine_Constrain.map_types\n") + val _ = Logger.debug1 ("map_types: f_cl = " ^ string_of_path (name_of h1) ^ "\n") + val _ = Logger.debug1 ("map_types: t_cl = " ^ string_of_path (name_of h2) ^ "\n") + val _ = Logger.debug1 ("map_types: f_op = " ^ name_of_op h3 ^ "\n") + val _ = Logger.debug1 ("map_types: t_op = " ^ name_of_op h4 ^ "\n") (* classifier of return type *) (* TODO: remove next trace lines *) - val _ = trace wgen ("Length of model: " ^ Int.toString (List.length(#1 model))^ ".\n") + val _ = Logger.debug1 ("Length of model: " ^ Int.toString (List.length(#1 model))^ ".\n") val ret_fC = class_of_type (#result (h3)) model - val _ = trace wgen ("map_types 2 \n") + val _ = Logger.debug1 ("map_types 2 \n") (* name of classifier of return type *) val ret_namefC = name_of ret_fC - val _ = trace wgen ("map_types_3: " ^ string_of_path (ret_namefC) ^ "\n") - val _ = trace wgen ("map_types_4: " ^ string_of_path fP ^ "\n") + val _ = Logger.debug1 ("map_types_3: " ^ string_of_path (ret_namefC) ^ "\n") + val _ = Logger.debug1 ("map_types_4: " ^ string_of_path fP ^ "\n") (* relative path of return type *) val new_path = substitute_package fP tP ret_namefC - val _ = trace wgen ("map_types_5: name of return type: " ^ string_of_path (ret_namefC) ^ "\n") + val _ = Logger.debug1 ("map_types_5: name of return type: " ^ string_of_path (ret_namefC) ^ "\n") val c1 = class_of (new_path) (model) handle _ => let @@ -265,9 +266,9 @@ fun map_types [] fP tP model = [] raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4^s5^s6) end (* name of the arguments *) - val _ = trace wgen ("map_types_6: " ^ string_of_path (name_of c1) ^ "\n") + val _ = Logger.debug1 ("map_types_6: " ^ string_of_path (name_of c1) ^ "\n") val arg_class_name1 = List.map (fn (a,b) => (name_of (class_of_type b model))) (arguments_of_op (h3)) - val _ = trace wgen ("map_types_7: \n") + val _ = Logger.debug1 ("map_types_7: \n") val c2 = List.map (fn a => let val rel_path = substitute_package fP tP a @@ -287,27 +288,27 @@ fun map_types [] fP tP model = [] end end ) arg_class_name1 - val _ = trace wgen ("map_types_8: \n") + val _ = Logger.debug1 ("map_types_8: \n") val res = (true)::(map_types tail fP tP model) - val _ = trace function_ends ("WFCPOG_Refine_Constrain.map_types\n") + val _ = Logger.info ("WFCPOG_Refine_Constrain.map_types\n") in res end fun check_syntax_help (model:Rep.Model as (clist,alist)) fromPath toPath = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.check_syntax_help\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.check_syntax_help\n") (* check public classes of the two packages *) val x = map_public_classes fromPath toPath model - val _ = trace wgen ("check syntax 2 \n") + val _ = Logger.debug1 ("check syntax 2 \n") (* check public methods of the public classes *) val y = List.concat (map_public_ops x) - val _ = trace wgen ("check syntax 3 \n") + val _ = Logger.debug1 ("check syntax 3 \n") (* check types of the public operations of public classes *) val z = map_types y fromPath toPath model - val _ = trace wgen ("check syntax 4 \n") + val _ = Logger.debug1 ("check syntax 4 \n") val res = List.all (fn a => a) z - val _ = trace function_ends ("WFCPOG_Refine_Constraint.check_syntax_help\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.check_syntax_help\n") in res end @@ -316,16 +317,16 @@ fun check_syntax_help (model:Rep.Model as (clist,alist)) fromPath toPath = fun check_syntax wfpo (model:Rep.Model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.check_syntax\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.check_syntax\n") val data = WFCPOG_RFM_Data.get wfpo - val _ = trace wgen (print_refine_args data) + val _ = Logger.debug1 (print_refine_args data) val packages = (#rfm_tuple data) val from = (#1 packages) val to = (#2 packages) val model_packages = all_packages_of_model model - val _ = trace wgen ("Packages of model: "^(String.concat (List.map (fn a => ((string_of_path a)^", ")) model_packages))^".\n") - val _ = trace wgen ("Abstract Package = "^(string_of_path from)^", contains "^(Int.toString (List.length(from)))^" strings.\n") - val _ = trace wgen ("Concrete Package = "^(string_of_path to)^", contains "^(Int.toString(List.length(from)))^" strings.\n") + val _ = Logger.debug1 ("Packages of model: "^(String.concat (List.map (fn a => ((string_of_path a)^", ")) model_packages))^".\n") + val _ = Logger.debug1 ("Abstract Package = "^(string_of_path from)^", contains "^(Int.toString (List.length(from)))^" strings.\n") + val _ = Logger.debug1 ("Concrete Package = "^(string_of_path to)^", contains "^(Int.toString(List.length(from)))^" strings.\n") val check = if ((member from model_packages) andalso (member to model_packages)) then check_syntax_help model from to handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s) @@ -338,7 +339,7 @@ fun check_syntax wfpo (model:Rep.Model as (clist,alist)) = in raise WFCPOG.WFC_FailedException (wfpo,s1^s2^s3^s4) end - val _ = trace function_ends ("WFCPOG_Refine_Constraint.check_syntax\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.check_syntax\n") in check end @@ -346,11 +347,11 @@ fun check_syntax wfpo (model:Rep.Model as (clist,alist)) = (* fun refine_operation abs_oper conc_oper abs_class conc_class model = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.refine_classifier\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_classifier\n") val state = Variable("mystate",OclState) val op_term = get_holocl_operation ("abs") abs_oper abs_class model val refine = OperationCall (op_term,DummyT,["holOclLib","Boolean","OclLocalValid"],[(state,OclState)],Boolean) - val _ = trace function_ends ("WFCPOG_Refine_Constraint.refine_classifier\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_classifier\n") in (["po_refine_"^(string_of_path (name_of abs_class))^"_"^(string_of_path (name_of conc_class))^"_"^(name_of_op abs_oper)],refine) end @@ -358,52 +359,52 @@ fun refine_operation abs_oper conc_oper abs_class conc_class model = fun refine_operation abs_oper conc_oper abs_class conc_class model = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.refine_classifier\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_classifier\n") val R = get_holocl_abstraction_relation abs_class conc_class model val S = get_holocl_operation ("abs") abs_oper abs_class model val T = get_holocl_operation ("conc") conc_oper conc_class model val refine = OperationCall(S,DummyT,["holOclLib","methodology","refinement","OclForwardRefinement"],[(T,DummyT),(R,DummyT)],Boolean) - val _ = trace function_ends ("WFCPOG_Refine_Constraint.refine_classifier\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_classifier\n") in (["po_refine_"^(string_of_path (name_of abs_class))^"_"^(string_of_path (name_of conc_class))^"_"^(name_of_op abs_oper)],refine) end fun refine_classifier abs_class conc_class model = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.refine_classifier\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_classifier\n") val abs_ops = List.filter (is_visible_op) (local_operations_of abs_class) val conc_ops = List.filter (is_visible_op) (local_operations_of conc_class) val gops = group_op (List.last (Rep_Core.name_of abs_class)) abs_ops conc_ops val res = List.map (fn (a,b) => refine_operation a b abs_class conc_class model) (gops) - val _ = trace function_ends ("WFCPOG_Refine_Constraint.refine_classifier\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_classifier\n") in res end fun refine_package abs_path conc_path (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.refine_package\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_package\n") val abs_classes = List.filter (fn a => (package_of a = abs_path) andalso (is_visible_cl a)) (clist) val conc_classes = List.filter (fn a => (package_of a = conc_path) andalso (is_visible_cl a)) (clist) val cl_grouped = group_cl abs_classes conc_classes val res = (List.concat (List.map (fn (a,b) => refine_classifier a b model) cl_grouped)) - val _ = trace function_ends ("WFCPOG_Refine_Constraint.refine_package\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.refine_package\n") in res end fun generate_pos wfpo (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.generate_pos\n") - val _ = trace wgen ("remove OclLib ...\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.generate_pos\n") + val _ = Logger.debug1 ("remove OclLib ...\n") val classes = removeOclLibrary clist - val _ = trace wgen ("oclLib removed ...\n") - val _ = trace wgen ("Extract args ...\n") + val _ = Logger.debug1 ("oclLib removed ...\n") + val _ = Logger.debug1 ("Extract args ...\n") val rfm_args = WFCPOG_RFM_Data.get wfpo val packages = (#rfm_tuple rfm_args) - val _ = trace wgen("Args extracted ...\n") + val _ = Logger.debug1("Args extracted ...\n") val res = refine_package (#1 packages) (#2 packages) model - val _ = trace function_ends ("WFCPOG_Refine_Constraint.generate_pos\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.generate_pos\n") in res end diff --git a/su4sml/src/wfcpog/rep_holocl.sml b/su4sml/src/wfcpog/rep_holocl.sml index a58a3e8..88b3f70 100644 --- a/su4sml/src/wfcpog/rep_holocl.sml +++ b/su4sml/src/wfcpog/rep_holocl.sml @@ -5,7 +5,8 @@ * holocl_namespace.sml --- * This file is part of HOL-OCL. * - * Copyright (c) 2008 Achim D. Brucker, Germany + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -288,20 +289,20 @@ fun holocl_localValid_transition term var_name1 var_name2 = fun get_holocl_operation abs_or_conc oper class model = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.get_holocl_operation\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.get_holocl_operation\n") val hol_name = string_of_path ((name_of class)@[name_of_op oper]) val styp = type_of class val src = Variable((abs_or_conc^"_"^(name_of_op oper)),styp) val predicate = Predicate(src,Boolean,[hol_name],args2varargs (map (fn (n,t) => (abs_or_conc^"_"^n,t)) (arguments_of_op oper))) - val _ = trace function_ends ("WFCPOG_Refine_Constraint.get_holocl_operation\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.get_holocl_operation\n") in predicate end fun get_holocl_abstraction_relation abs_class conc_class model = let - val _ = trace function_calls ("WFCPOG_Refine_Constraint.get_holocl_abstraction_relation\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.get_holocl_abstraction_relation\n") val predicate_name = "R_"^(string_of_path (package_of abs_class))^"_"^(string_of_path (package_of conc_class))^"_"^(List.last (name_of abs_class)) val abs_typ = type_of abs_class val conc_typ = type_of conc_class @@ -310,7 +311,7 @@ fun get_holocl_abstraction_relation abs_class conc_class model = val abs_term = Variable(string_of_path (name_of abs_class),abs_typ) val conc_term = Variable(string_of_path (name_of conc_class),conc_typ) val predicate = Predicate(abs_state,OclState,[predicate_name],[(conc_state,OclState),(abs_term,abs_typ),(conc_term,conc_typ)]) - val _ = trace function_ends ("WFCPOG_Refine_Constraint.get_holocl_abstraction_relation\n") + val _ = Logger.info ("WFCPOG_Refine_Constraint.get_holocl_abstraction_relation\n") in predicate end diff --git a/su4sml/src/wfcpog/taxonomy_consistency.sml b/su4sml/src/wfcpog/taxonomy_consistency.sml index 6b32128..323a1c1 100644 --- a/su4sml/src/wfcpog/taxonomy_consistency.sml +++ b/su4sml/src/wfcpog/taxonomy_consistency.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -120,7 +121,7 @@ fun deep_of_classifier x (Class{parent,...}) (model as (clist,alist)) = fun check_depth_classifier depth class (model as (clist,alist)) = let - val _ = trace wgen ("look for deep ...\n") + val _ = Logger.debug1 ("look for deep ...\n") val d = deep_of_classifier 0 class model val check = if (depth >= d) @@ -138,14 +139,14 @@ fun check_depth_classifier depth class (model as (clist,alist)) = fun check_depth wfpo (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPG_Taxonomy_Consistency.check_maxDepth\n") + val _ = Logger.info ("WFCPG_Taxonomy_Consistency.check_maxDepth\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a) orelse (is_Iface a) orelse (is_Enum a) orelse (is_Primi a)) cl val tax_args = WFCPOG_TAX_Data.get wfpo val depth = (#max_depth tax_args) val res = List.all (fn a => a = true) (List.map (fn a => check_depth_classifier depth a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s)) classes) - val _ = trace function_calls ("WFCPG_Taxonomy_Consistency.check_maxDepth\n") + val _ = Logger.info ("WFCPG_Taxonomy_Consistency.check_maxDepth\n") in res end diff --git a/su4sml/src/wfcpog/test-data.sml b/su4sml/src/wfcpog/test-data.sml index 02dcd06..68b5154 100644 --- a/su4sml/src/wfcpog/test-data.sml +++ b/su4sml/src/wfcpog/test-data.sml @@ -18,7 +18,7 @@ structure TAX_Data = WFCPOG_Taxonomy_Constraint.WFCPOG_TAX_Data val wfc_inf_nameclashes = get_wfpo supported_wfs "wfc_inf_nameclashes" val wfc_inf_stereotypes = get_wfpo supported_wfs "wfc_inf_stereotypes" val wfc_inf_all = get_wfpo supported_wfs "wfc_inf_all" -val _ = trace high ("............. interface constraint loaded ...\n") +val _ = Logger.info ("............. interface constraint loaded ...\n") (** VISIBILITY CONSTRAINT **) val wfc_vis_class = get_wfpo supported_wfs "wfc_vis_class" @@ -26,19 +26,19 @@ val wfc_vis_inheritance = get_wfpo supported_wfs "wfc_vis_inheritance" val wfc_vis_runtime = get_wfpo supported_wfs "wfc_vis_runtime" val wfc_vis_design_by_contract = get_wfpo supported_wfs "wfc_vis_design_by_contract" val wfc_vis_all = get_wfpo supported_wfs "wfc_vis_all" -val _ = trace high ("............. visibility constraint loaded ...\n") +val _ = Logger.info ("............. visibility constraint loaded ...\n") (* TAXONOMY CONSTRAINT *) val wfc_tax = get_wfpo supported_wfs "wfc_tax" val wfc_tax_5 = rename_wfpo "wfc_tax_5" (TAX_Data.put ({key=2,max_depth=5}) wfc_tax) -val _ = trace high ("............. taxonomy constraint loaded ...\n") +val _ = Logger.info ("............. taxonomy constraint loaded ...\n") (** REFINEMENT CONSTRAINT **) val wfc_rfm = get_wfpo supported_wfs "wfc_rfm" -val _ = trace high ("............. refinement constraints loaded ...\n") +val _ = Logger.info ("............. refinement constraints loaded ...\n") val wfc_rfm_SC = rename_wfpo "wfc_rfm_SC" (RFM_Data.put ({key=10,rfm_tuple=(["AbstractSimpleChair04"],["ConcreteSimpleChair02"])}) wfc_rfm) val wfc_rfm_SR= rename_wfpo "wfc_rfm_SR" (RFM_Data.put ({key=10,rfm_tuple=(["AbstractOverriding"],["ConcreteOverriding"])}) wfc_rfm) -val _ = trace high ("............. refine wfc constraint loaded ...\n") +val _ = Logger.info ("............. refine wfc constraint loaded ...\n") (** QUERY CONSISTENCY **) val wfc_quy_strong = get_wfpo supported_wfs "wfc_quy_strong" @@ -54,37 +54,37 @@ val po_lsk_pre = get_wfpo supported_pos "po_lsk_pre" val po_lsk_post = get_wfpo supported_pos "po_lsk_post" val po_lsk_inv = get_wfpo supported_pos "po_lsk_inv" val po_lsk_all = get_wfpo supported_pos "po_lsk_all" -val _ = trace high ("............. liskov constraint loaded ...\n") +val _ = Logger.info ("............. liskov constraint loaded ...\n") (** DATA MODEL CONSTRAINT **) val po_cm = get_wfpo supported_pos "po_class_model" val po_sm = get_wfpo supported_pos "po_strong_model" -val _ = trace high ("............. data model constraint loaded ...\n") +val _ = Logger.info ("............. data model constraint loaded ...\n") (** OPERATIONAL CONSTRAINT **) val po_om = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "po_oper_model" -val _ = trace high ("............. operational constraint loaded ...\n") +val _ = Logger.info ("............. operational constraint loaded ...\n") (** CONSTRUCTOR CONSTRAINT **) val po_cstr_post = get_wfpo supported_pos "po_cstr_post" val po_cstr_attribute = get_wfpo supported_pos "po_cstr_attribute" val po_cstr_all = get_wfpo supported_pos "po_cstr_all" -val _ = trace high ("............. constructor constraints loaded ...\n") +val _ = Logger.info ("............. constructor constraints loaded ...\n") (** COMMAND/QUERY CONSTRAINT **) (* val po_cmd = get_wfpo supported_pos "po_" val po_quy = get_wfpo supported_pos "po_quy" *) -val _ = trace high ("............. command/query constraints loaded ...\n") +val _ = Logger.info ("............. command/query constraints loaded ...\n") (** REFINEMENT CONSTRAINT **) val po_rfm = get_wfpo supported_pos "po_rfm" -val _ = trace high ("............. refinement constraints loaded ...\n") +val _ = Logger.info ("............. refinement constraints loaded ...\n") val po_rfm_SC = rename_wfpo "po_rfm_SR" (RFM_Data.put ({key=10,rfm_tuple=(["AbstractSimpleChair04"],["ConcreteSimpleChair02"])}) po_rfm) -val _ = trace high ("............. refine pog constraint loaded ...\n") +val _ = Logger.info ("............. refine pog constraint loaded ...\n") val po_rfm_SR = rename_wfpo "po_rfm_SR" (RFM_Data.put ({key=10,rfm_tuple=(["AbstractOverriding"],["ConcreteOverriding"])}) po_rfm) -val _ = trace high ("............. refine pog constraint loaded ...\n") +val _ = Logger.info ("............. refine pog constraint loaded ...\n") (* ALL CONSTRAINTS: *) diff --git a/su4sml/src/wfcpog/test-suite.sml b/su4sml/src/wfcpog/test-suite.sml index 95ddd11..4d23f6f 100644 --- a/su4sml/src/wfcpog/test-suite.sml +++ b/su4sml/src/wfcpog/test-suite.sml @@ -135,7 +135,7 @@ fun start_tests model [] = [] case (apply_of h) of WFC (a) => let - val _ = trace wgen ("Testing a wellformed constraint: \n") + val _ = Logger.info ("Testing a wellformed constraint: \n") val res_wfcs = check_wfcs model [h] handle WFCPOG.WFC_FailedException (wfc,s) => let @@ -148,29 +148,29 @@ fun start_tests model [] = [] case check of false => let - val _ = trace wgen ("test is false ...\n") + val _ = Logger.info ("test is false ...\n") val mes = ("\n" ^ (name_of h) ^ (insert_dots (name_of h)) ^ "[FAILED]\n") - val _ = trace wgen mes + val _ = Logger.info mes val _ = buffer:=(!buffer)^mes - val _ = trace wgen ("results logged in buffer ...\n") + val _ = Logger.info ("results logged in buffer ...\n") in ([])@(start_tests model wfpos) end | true => let - val _ = trace wgen ("test is true ...\n") + val _ = Logger.info ("test is true ...\n") val name = WFCPOG.name_of h val mes = ("\n" ^ name ^ (insert_dots (name)) ^ "[OK]\n") - val _ = trace wgen mes + val _ = Logger.info mes val _ = buffer:=(!buffer)^mes - val _ = trace wgen ("results logged in buffer ...\n") + val _ = Logger.info ("results logged in buffer ...\n") in ([])@(start_tests model wfpos) end end | POG (a) => let - val _ = trace wgen ("Testing a proof obligation constraint: \n") + val _ = Logger.info ("Testing a proof obligation constraint: \n") val pos = generate_pos model [h] handle WFCPOG.WFC_FailedException (po,s) => let @@ -205,9 +205,9 @@ fun test (tc:testcase) wfs pos = val (clist,alist) = Rep_Core.normalize_ext 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 _ = Logger.info ("Model of testcase loaded ...\n") val x = start_tests model (wfs@pos) - val _ = trace wgen ("Test finished ...\n") + val _ = Logger.info ("Test finished ...\n") in x @@ -227,10 +227,10 @@ fun print_tc (tc:testcase)= fun runTest name wfs pos = let - val _ = trace wgen ("Starts runing one test ...\n") + val _ = Logger.info ("Starts runing one test ...\n") val _ = reset_buffer() val tc = valOf (List.find (fn a => name = (#name a)) testcases) - val _ = trace wgen ("Accessing model ...\n") + val _ = Logger.info ("Accessing model ...\n") val s1 = (print_tc tc) val _ = (test tc wfs pos) val _ = buffer:=s1^(!buffer) @@ -244,7 +244,7 @@ fun runTest name wfs pos = fun runTests wfs pos = let - val _ = trace wgen ("Starts running tests ...\n") + val _ = Logger.info ("Starts running tests ...\n") val _ = reset_buffer() val _ = List.map (fn a => let @@ -263,10 +263,10 @@ fun runTests wfs pos = fun runTest_ret_pos name wfs pos = let - val _ = trace wgen ("Starts runing one test ...\n") + val _ = Logger.info ("Starts runing one test ...\n") val _ = reset_buffer() val tc = valOf (List.find (fn a => name = (#name a)) testcases) - val _ = trace wgen ("Accessing model ...\n") + val _ = Logger.info ("Accessing model ...\n") val s1 = (print_tc tc) val pos = List.concat (test tc wfs pos) val _ = buffer:=s1^(!buffer) @@ -281,7 +281,7 @@ fun runTest_ret_pos name wfs pos = fun runTests_ret_pos wfs pos = let - val _ = trace wgen ("Starts running tests ...\n") + val _ = Logger.info ("Starts running tests ...\n") val _ = reset_buffer() val pos = List.concat (List.concat (List.map (fn a => let diff --git a/su4sml/src/wfcpog/visibility_consistency.sml b/su4sml/src/wfcpog/visibility_consistency.sml index 0941dff..7165ebb 100644 --- a/su4sml/src/wfcpog/visibility_consistency.sml +++ b/su4sml/src/wfcpog/visibility_consistency.sml @@ -5,7 +5,8 @@ * context_declarations.sml --- * This file is part of su4sml. * - * Copyright (c) 2005-2007, ETH Zurich, Switzerland + * Copyright (c) 2005-2007 ETH Zurich, Switzerland + * 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -118,12 +119,12 @@ and expr_is_visible modif (Literal(s,typ)) model = true andalso expr_is_visible modif then_t model | expr_is_visible modif (AssociationEndCall(src,styp,path,rtyp)) model = let - val _ = trace wgen ("start expr_is_visible") + val _ = Logger.info ("start expr_is_visible") val cl = class_of_term src model val att_name = List.last(path) - val _ = trace wgen ("start get_associationends ") + val _ = Logger.info ("start get_associationends ") val att = get_associationend att_name cl model - val _ = trace wgen ("end expr_is_visible") + val _ = Logger.info ("end expr_is_visible") in if (visibility_conforms_to (#visibility att) modif) then (expr_is_visible modif src model) @@ -131,29 +132,29 @@ and expr_is_visible modif (Literal(s,typ)) model = true end | expr_is_visible modif (x as OperationCall(src,styp,path,args,rtyp)) model = let - val _ = trace function_calls ("WFCPGO_Visibility_Constraint.expr_is_visible : " ^ (ocl2string false x) ^ "\n") + val _ = Logger.debug1 ("WFCPGO_Visibility_Constraint.expr_is_visible : " ^ (ocl2string false x) ^ "\n") val typ = type_of_term src val cl = class_of_term (Variable("x",typ)) model val op_name = List.last(path) - val _ = trace 50 ("Classifier : " ^ (string_of_path (name_of cl)) ^ "\n") - val _ = trace 50 ("Op_name : " ^ op_name ^ "\n") + val _ = Logger.info ("Classifier : " ^ (string_of_path (name_of cl)) ^ "\n") + val _ = Logger.info ("Op_name : " ^ op_name ^ "\n") val oper = get_operation op_name cl model - val _ = trace wgen ("got operation\n") + val _ = Logger.info ("got operation\n") val res = if (visibility_conforms_to (#visibility oper) modif) then ((List.all (fn (a,b) => (expr_is_visible modif a model)) args) andalso (expr_is_visible modif src model)) else false - val _ = trace function_ends ("WFCPGO_Visibility_Constraint.expr_is_visible\n") + val _ = Logger.debug1 ("WFCPGO_Visibility_Constraint.expr_is_visible\n") in res end | expr_is_visible modif (x as AttributeCall(src,styp,path,rtyp)) model = let - val _ = trace 50 ("expr_is_visible: AttCall \n ") + val _ = Logger.info ("expr_is_visible: AttCall \n ") val cl = class_of_term src model val att_name = List.last(path) val att = get_attribute att_name cl model - val _ = trace 100 ("end expr_is_visible") + val _ = Logger.info ("end expr_is_visible") in if (visibility_conforms_to (#visibility att) modif) then (expr_is_visible modif src model) @@ -228,7 +229,7 @@ fun check_inheritance_classifier class model = raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4) end ) mod_ops_super_this - val _ = trace function_ends ("WFCPOG_Visibility_Consistency.check_inheritance_visibility_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Consistency.check_inheritance_visibility_consistency\n") in List.all (fn a => a = true) check end @@ -328,26 +329,26 @@ fun check_design_classifier class model = fun model_entity_consistency wfc_sel (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Visibility_Constraint.model_entity_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.model_entity_consistency\n") (* remove OclLibrary *) val cl = removeOclLibrary (clist) (* visiblity only for Classes and AssocClasses *) val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl val res = List.all (fn a => a = true) (List.map (fn a => check_entity_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s)) classes) - val _ = trace function_ends ("WFCPOG_Visibility_Constraint.model_entity_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.model_entity_consistency\n") in res end fun model_inheritance_consistency wfc_sel (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Visibility_Constraint.model_inheritance_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.model_inheritance_consistency\n") val cl = removeOclLibrary (clist) val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl val res = List.all (fn a => a = true) (List.map (fn a => check_inheritance_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s)) classes) - val _ = trace function_ends ("WFCPOG_Visibility_Constraint.model_inheritance_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.model_inheritance_consistency\n") in res @@ -355,24 +356,24 @@ fun model_inheritance_consistency wfc_sel (model as (clist,alist)) = fun constraint_check_by_runtime_consistency wfc_sel (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Visibility_Constraint.constraint_check_by_runtime_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.constraint_check_by_runtime_consistency\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl val res = List.all (fn a => a = true) (List.map (fn a => check_runtime_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s)) classes) - val _ = trace function_ends ("WFCPOG_Visibility_Constraint.constraint_check_by_runtime_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.constraint_check_by_runtime_consistency\n") in res end fun constraint_design_by_contract_consistency wfc_sel (model as (clist,alist)) = let - val _ = trace function_calls ("WFCPOG_Visibility_Constraint.constraint_design_by_contract_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.constraint_design_by_contract_consistency\n") val cl = removeOclLibrary clist val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl val res = List.all (fn a => a = true) (List.map (fn a => check_design_classifier a model handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s)) classes) - val _ = trace function_calls ("WFCPOG_Visibility_Constraint.constraint_design_by_contract_consistency\n") + val _ = Logger.debug1 ("WFCPOG_Visibility_Constraint.constraint_design_by_contract_consistency\n") in res diff --git a/su4sml/src/wfcpog/wfcpog.sml b/su4sml/src/wfcpog/wfcpog.sml index df4f3d3..3d6e0b6 100644 --- a/su4sml/src/wfcpog/wfcpog.sml +++ b/su4sml/src/wfcpog/wfcpog.sml @@ -5,7 +5,7 @@ * wfcpog.sml --- * This file is part of su4sml. * - * Copyright (c) 2008 Achim D. Brucker, Germany + * Copyright (c) 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * diff --git a/su4sml/src/wfcpog/wfcpog_registry.sml b/su4sml/src/wfcpog/wfcpog_registry.sml index 0c048db..5b0b82c 100644 --- a/su4sml/src/wfcpog/wfcpog_registry.sml +++ b/su4sml/src/wfcpog/wfcpog_registry.sml @@ -5,7 +5,7 @@ * --- * This file is part of su4sml. * - * Copyright (c) 2008 Achim D. Brucker, Germany + * Copyright (c) 2008-2009 Achim D. Brucker, Germany * * All rights reserved. * @@ -128,7 +128,7 @@ fun del_wfpo wfpo_id = ((wfpos := List.filter (fn w => not ((WFCPOG.id_of w) = ( fun get_wfpo [] x = let - val _ = trace exce ("No ID = " ^ x ^ " found in given list!\n") + val _ = Logger.warn ("No ID = " ^ x ^ " found in given list!\n") in raise WFCPOG_RegistryError ("No ID = " ^ x ^ " found in given list!\n") end @@ -470,20 +470,20 @@ fun set_data (new_data:Object.T table) (WFCPOG.WFPO{identifier,name,description, fun check_wfc model wfc = let - val _ = trace function_calls ("WFCPOG_Registry.check_wfc\n") - val _ = trace wgen (name_of wfc ^ ".............." ^ "\n") + val _ = Logger.info ("WFCPOG_Registry.check_wfc\n") + val _ = Logger.debug1 (name_of wfc ^ ".............." ^ "\n") val res = case (WFCPOG.apply_of wfc) of WFCPOG.WFC(a) => (wfc,a wfc model) | x => raise WFCPOG_RegistryError ("A assumed wfc " ^ (name_of wfc) ^ " is not a wfc!\n") - val _ = trace function_ends ("WFCPOG_Registry.check_wfc\n") + val _ = Logger.info ("WFCPOG_Registry.check_wfc\n") in res end fun check_wfcs model wfcs = let - val _ = trace function_calls ("WFCPOG_Registry.check_wfcs\n") + val _ = Logger.info ("WFCPOG_Registry.check_wfcs\n") val res = List.concat (map (fn (a as WFCPOG.WFPO{identifier,name,description,recommended,depends,recommends,apply,data}:WFCPOG.wfpo) => if (depends = []) then [(check_wfc model a)] @@ -503,27 +503,27 @@ fun check_wfcs model wfcs = then raise WFCPOG_RegistryError ("A wellformedness check has a proof obligation marked as depending. But this is not allowed! \n\nCHANGE WFCPOG_Registry.supported_wfs ENTRY(IES)!!!") else (List.map (check_wfc model) depending_wfcs)@[(check_wfc model a)] end) wfcs) - val _ = trace function_ends ("WFCPOG_Registry.check_wfcs\n") + val _ = Logger.info ("WFCPOG_Registry.check_wfcs\n") in res end fun generate_po model po = let - val _ = trace function_calls ("WFCPOG_Registry.generate_po\n") - val _ = trace wgen (name_of po ^ " ...............\n") + val _ = Logger.info ("WFCPOG_Registry.generate_po\n") + val _ = Logger.debug1 (name_of po ^ " ...............\n") val res = case (WFCPOG.apply_of po) of WFCPOG.POG (a) => (po,a po model) | x => raise WFCPOG_RegistryError ("A assumed po " ^ (name_of po) ^ " is not a po!\n") - val _ = trace function_ends ("WFCPOG_Registry.generate_po\n") + val _ =Logger.info ("WFCPOG_Registry.generate_po\n") in res end fun generate_pos model pos = let - val _ = trace function_calls ("WFCPOG_Registry.generate_pos\n") + val _ = Logger.info ("WFCPOG_Registry.generate_pos\n") val res = List.concat (map (fn (a as (WFCPOG.WFPO{identifier,name,description,recommended,depends,recommends,apply,data}:WFCPOG.wfpo)) => if (depends = []) @@ -546,7 +546,7 @@ fun generate_pos model pos = else (* doesn't matter, because WFCPOG_WFC_FailedException is returned *) [] end) pos) - val _ = trace function_ends ("WFCPOG_Registry.generate_pos\n") + val _ = Logger.info ("WFCPOG_Registry.generate_pos\n") in res end