Merge pull request kind2-mc#1065 from lorchrob/cand-gen-prop-output

Give more detailed information about property types in all output formats

schemas/kind2-output.json

@@ -649,6 +649,9 @@
                         "PropAnnot"
                     ]
                 },
+                "isCandidate": {
+                    "type": "boolean"
+                },
                 "runtime": {
                     "$ref": "#/definitions/runtime"
                 },

schemas/kind2-output.xsd

@@ -22,6 +22,19 @@
     </xs:restriction>
   </xs:simpleType>
 
+  <!-- Property source-->
+  <xs:simpleType name="PropSource">
+    <xs:restriction base="xs:string">
+      <xs:enumeration value="Assumption"/>
+      <xs:enumeration value="Guarantee"/>
+      <xs:enumeration value="Generated"/>
+      <xs:enumeration value="NonVacuityCheck"/>
+      <xs:enumeration value="OneModeActive"/>
+      <xs:enumeration value="Ensure"/>
+      <xs:enumeration value="PropAnnot"/>
+    </xs:restriction>
+  </xs:simpleType>
+
   <!-- Context of realizability check -->
   <xs:simpleType name="Context">
     <xs:restriction base="xs:string">
@@ -355,7 +368,8 @@
     <xs:attribute name="line" type="NonNegativeInteger"/>
     <xs:attribute name="column" type="NonNegativeInteger"/>
     <xs:attribute name="scope" type="xs:string"/>
-    <xs:attribute name="source" type="xs:string"/>
+    <xs:attribute name="source" type="PropSource"/>
+    <xs:attribute name="isCandidate" type="xs:boolean"/>
   </xs:complexType>
 
   <xs:complexType name="PostAnalysisStartType">

src/kEvent.ml

@@ -311,7 +311,14 @@ let proved_pt mdl level trans_sys k prop =
   if 
     not (Property.prop_status_known (TransSys.get_prop_status trans_sys prop))
   then (
-    let cand_or_prop = (if TransSys.is_candidate trans_sys prop then  "Candidate" else "Property") in
+
+    let property = TransSys.property_of_name trans_sys prop in
+    let prop_type = match property.prop_source with 
+      | Candidate None -> "Candidate property"
+      | Candidate Some (Generated _) -> "Generated candidate property"
+      | Generated _ -> "Generated property"
+      | _ -> "Property"
+    in
     let k_val = (function ppf -> match k with
       | None -> ()
       | Some k -> Format.fprintf ppf "for k=%d " k) in
@@ -322,7 +329,7 @@ let proved_pt mdl level trans_sys k prop =
         !log_ppf
         "@[<hov>%t %s @{<blue_b>%s@} is valid %tby %a after %.3fs.@.@."
         success_tag
-        cand_or_prop
+        prop_type
         prop
         k_val
         pp_print_kind_module_pt mdl
@@ -332,7 +339,7 @@ let proved_pt mdl level trans_sys k prop =
         !log_ppf
         ("@[<hov>%t %s @{<blue_b>%s@} is unreachable in %d steps or more %tby %a after %.3fs.@.@.")
         failure_tag
-        cand_or_prop
+        prop_type
         prop
         ts
         k_val
@@ -343,7 +350,7 @@ let proved_pt mdl level trans_sys k prop =
         !log_ppf
         "@[<hov>%t %s @{<blue_b>%s@} is unreachable in %d steps or less %tby %a after %.3fs.@.@."
         failure_tag
-        cand_or_prop
+        prop_type
         prop
         ts
         k_val
@@ -354,7 +361,7 @@ let proved_pt mdl level trans_sys k prop =
         !log_ppf
         "@[<hov>%t %s @{<blue_b>%s@} is unreachable at step %d %tby %a after %.3fs.@.@."
         failure_tag
-        cand_or_prop
+        prop_type
         prop
         ts
         k_val
@@ -365,7 +372,7 @@ let proved_pt mdl level trans_sys k prop =
         !log_ppf
         "@[<hov>%t %s @{<blue_b>%s@} is unreachable between steps %d and %d %tby %a after %.3fs.@.@."
         failure_tag
-        cand_or_prop
+        prop_type
         prop
         ts1
         ts2
@@ -377,7 +384,7 @@ let proved_pt mdl level trans_sys k prop =
         !log_ppf
         "@[<hov>%t %s @{<blue_b>%s@} is unreachable %tby %a after %.3fs.@.@."
         failure_tag
-        cand_or_prop
+        prop_type
         prop
         k_val
         pp_print_kind_module_pt mdl
@@ -796,8 +803,7 @@ let prop_attributes_xml trans_sys prop_name =
     )
     | Property.Candidate None -> ""
     | Property.Candidate (Some source) -> get_attributes source
-    | Property.Instantiated (_, prop) ->
-        get_attributes prop.Property.prop_source
+    | Property.Instantiated (_, prop) -> get_attributes prop.Property.prop_source
     | Property.Assumption (pos, (scope, _)) ->
         let fname, lnum, cnum = file_row_col_of_pos pos in
         Format.asprintf " line=\"%d\" column=\"%d\" scope=\"%s\" source=\"Assumption\"%a"
@@ -820,7 +826,8 @@ let prop_attributes_xml trans_sys prop_name =
           lnum cnum (String.concat "." scope) pp_print_fname fname
   in
 
-  get_attributes prop.Property.prop_source
+  " isCandidate=\"" ^ (string_of_bool (Property.is_candidate prop.Property.prop_source)) 
+  ^ "\"" ^ get_attributes prop.Property.prop_source
 
 
 (* Output proved property as XML *)
@@ -1161,6 +1168,9 @@ let prop_attributes_json ppf trans_sys prop_name =
     | Property.Candidate (Some source) -> get_attributes source
   in
 
+  Format.fprintf ppf "\"isCandidate\" : \"%s\",@,"
+      (string_of_bool (Property.is_candidate prop.Property.prop_source));
+
   get_attributes prop.Property.prop_source
 
 

src/property.ml

@@ -100,6 +100,11 @@ and prop_source =
      properties *)
   | Candidate of prop_source option
 
+let is_candidate = function 
+| Candidate _ -> true
+| PropAnnot _ | Generated _ | Instantiated _ | Assumption _ 
+| Guarantee _ | GuaranteeOneModeActive _ | GuaranteeModeImplication _
+| NonVacuityCheck _ -> false
 
 let copy t = { t with prop_status = t.prop_status }
 

src/property.mli

@@ -103,6 +103,9 @@ val copy : t -> t
 (** Pretty-prints a property source. *)
 val pp_print_prop_source : Format.formatter -> prop_source -> unit
 
+(** Returns true iff the input property source is candidate *)
+val is_candidate : prop_source -> bool
+
 (** Pretty-prints a property status. *)
 val pp_print_prop_status : Format.formatter -> prop_status -> unit