Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fixes for commit 1cbc4d1 #1076

Merged
merged 1 commit into from
Jun 14, 2024
Merged

Fixes for commit 1cbc4d1 #1076

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 15 additions & 15 deletions src/kEvent.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -307,12 +307,12 @@ let tag_pt level tag str =

(* Output proved property as plain text *)
let proved_pt mdl level trans_sys k prop =

let property = TransSys.property_of_name trans_sys prop in
(* Only output if status was unknown *)
if
not (Property.prop_status_known (TransSys.get_prop_status trans_sys prop))
not (Property.prop_status_known (Property.get_prop_status property))
then (

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"
Expand Down Expand Up @@ -2229,7 +2229,7 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
(* Property found true for k steps *)
| (m, PropStatus (p, (Property.PropKTrue k as s))) :: tl -> (

try
try (
(* Change property status in transition system *)
TransSys.set_prop_ktrue trans_sys k p;

Expand All @@ -2239,21 +2239,21 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
invars
((m, (p, s)) :: prop_status)
tl

)
with TransSys.PropertyNotFound _->
(* Continue without changes *)
update_trans_sys' trans_sys invars prop_status tl
)
(* Property found invariant *)
| (m, PropStatus (p, (Property.PropInvariant cert as s))) :: tl -> (

try
(* Change property status (of all instances with name [p]) *)
TransSys.set_prop_invariant trans_sys p cert;

try (
(* Output proved property *)
log_proved m L_warn trans_sys None p;

(* Change property status (of all instances with name [p]) *)
TransSys.set_prop_invariant trans_sys p cert;

let term =
TransSys.props_list_of_bound trans_sys Numeral.zero
|> List.assoc p
Expand Down Expand Up @@ -2292,28 +2292,28 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
invars
( (m, (p, s)) :: prop_status )
tl

)
with TransSys.PropertyNotFound _->
(* Continue without changes *)
update_trans_sys' trans_sys invars prop_status tl
)
(* Property found false *)
| (m, PropStatus (p, (Property.PropFalse cex as s))) :: tl -> (

try
(* Change property status in transition system *)
TransSys.set_prop_false trans_sys p cex;

try (
(* Output disproved property *)
log_cex true m L_warn input_sys analysis trans_sys p cex ;

(* Change property status in transition system *)
TransSys.set_prop_false trans_sys p cex;

(* Continue with property status added to accumulator *)
update_trans_sys'
trans_sys
invars
((m, (p, s)) :: prop_status)
tl

)
with TransSys.PropertyNotFound _->
(* Continue without changes *)
update_trans_sys' trans_sys invars prop_status tl
Expand Down
9 changes: 6 additions & 3 deletions src/transSys.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1338,9 +1338,12 @@ let init_define_fun_declare_vars_of_bounds t define declare lbound ubound =
let property_of_name t name =

(* Return the first property with the given name *)
List.find
(fun { P.prop_name } -> prop_name = name )
t.properties
try
List.find
(fun { P.prop_name } -> prop_name = name )
t.properties
with Not_found ->
raise (PropertyNotFound name)


(* Get term of property by name *)
Expand Down
Loading