From 4637db06583bc250b96e6145fc7bac9e16c730df Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 1 Aug 2017 11:10:01 +0200 Subject: Fixes is_accessed_by. CNE_01700 is not working. The BCE has been updated to include a group of items that should be tagged by the CNE_01700 rule. However, it's not happening. I don't see anything wrong with the way the CNE_01700 rule is written and a quick overview of the generated model would lead me to conclude that it indeed should tag something. Likely there are still issues with the way properties are turned into Kodkod formulas. --- data/ast/best_chronometer_ever.xml | 22389 ++++++++++++++++------------------- data/level/structural_level.lvl | 3 + data/property/cnes/CNE_01700.pro | 76 +- 3 files changed, 9989 insertions(+), 12479 deletions(-) (limited to 'data') diff --git a/data/ast/best_chronometer_ever.xml b/data/ast/best_chronometer_ever.xml index 4b597a8..89491ae 100644 --- a/data/ast/best_chronometer_ever.xml +++ b/data/ast/best_chronometer_ever.xml @@ -6124,7 +6124,7 @@ seen_flag="false" has_parameter="false" hide_implicit_flag="false" pure_flag="false" foreign_flag="false" visible_flag="true" - is_within_flag="false" use_flag="true" + is_within_flag="false" use_flag="false" resolution_function_flag="false" has_pure="false" has_body="false" wait_state="unknown" all_sensitized_state="???"> @@ -8176,58 +8176,58 @@ identifier="work" date="10" library_directory="" elab_flag="false" visible_flag="true"> - - - + - - - + + - - - + - - - + - + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - + - + - - - + - - + - + - - - + - - - + + + - + - - - + + + + + + + + + + + + + + + + + + + - - - + + + - + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - + - - - + + + - - - - + + - - - + + + - + @@ -8656,164 +8693,164 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - + - - - + + - - - - - + + + - - + + - - - + - - - + + + - - - - - + + + @@ -8824,201 +8861,369 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - + + + - - + - - + - - - + + + - - + - - - + + + - - - + + + - - + - - + - - - + - - - + + + - - + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + - - + - - + + - + - + - - - + - - - + + - - - + - - - + - + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + - + - + - - + + - @@ -9159,10 +9364,10 @@ - + - - - - + + - + - + - - + + - @@ -9203,10 +9408,10 @@ - + - - - - + + - + - + - - + + - @@ -9247,10 +9452,10 @@ - + - - - - + + - + - + - - + + - @@ -9291,86 +9496,86 @@ - + - + - + - - - + - - + - + - - - + - - - + + + - + - - - - + + - + - + - - + + - @@ -9379,40 +9584,40 @@ - + - - - - + + - + - + - - + + - @@ -9421,40 +9626,40 @@ - + - - - - + + - + - + - - + + - @@ -9463,40 +9668,40 @@ - + - - - - + + - + - + - - + + - @@ -9505,66 +9710,66 @@ - + - - + - - - + - - - - + + + - - + - - - + + + - - - + + - - - + + + - - + @@ -9572,167 +9777,167 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - + - - - - + + + - - - - + - - - + + + - - + @@ -9741,55 +9946,54 @@ - - - - + - - - + + + - - - - - - + + + - @@ -9809,81 +10013,81 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + + - - - + + + - - + @@ -9891,135 +10095,135 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - - - + + + - @@ -10027,60 +10231,60 @@ - - - + - - - - + + + - - - - + - - - + + + - - + @@ -10089,55 +10293,54 @@ - - - - + - - - + + + - - - - - - + + + - @@ -10157,81 +10360,81 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + + - - - + + + - - + @@ -10239,142 +10442,142 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - - - - + + + - - + - - - + + + - - - - - + + + - - + - - - + + + - - - - - + + + - @@ -10382,24 +10585,24 @@ - - - - - + + + - @@ -10407,60 +10610,60 @@ - - - + - - - - + + + - - - - + - - - + + + - - + @@ -10469,55 +10672,54 @@ - - - - + - - - + + + - - - - - - + + + - @@ -10537,81 +10739,81 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + @@ -10619,176 +10821,174 @@ - - - - + - - - + + - - - - - + + + - - + + - - - + + - - - - + file="src/time_wizard.vhd" line="109" + col="35" expr_staticness="none"> - - - - + + + - - + - - - + + + - + file="src/time_wizard.vhd" line="110" + col="35" expr_staticness="none"> - - - - + + + - - + - - - + + + - - - - - + + + - - - - - - + + + - @@ -10796,24 +10996,24 @@ - - - - - + + + - @@ -10821,48 +11021,47 @@ - - - + - - - + + + - - + file="src/time_wizard.vhd" line="116" + col="32" expr_staticness="none"> - - - - + + + - @@ -10879,191 +11078,191 @@ - - - - - + + + + + - - - - + + + + - - + - - - + - - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - - - + + + - - - - + + - - - + + + - - + - - - + + + - - - - + - + - - + - - - + + + @@ -11072,1041 +11271,1037 @@ - - - - - + + + + + - - + - + - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + - - - + - - - + + + - - + - - - + + + - - + + - - + - - + + - + - + - - - + - - - + + - - - + - - - + - + - - + + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - + + + - - - + + + - + + + + + + + + + + + + + + + + + + + - + + + + + - - - - - - - - - - - - - - - + + + - - - + + + - + + + + + + + + + + + + + + + + + + + - + + + + + - - - + + - - - - + + + - - + - - + - - - + + - - - + + + - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - - - - + expr_staticness="global" name_staticness="local"> + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + - - - - - - + expr_staticness="global" name_staticness="local"> + + + + + + + + + + + + + + + + + + + + + + + + + + - + + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + has_signal_flag="true" type_staticness="local"> + + - - - - + + - - + + - @@ -12115,542 +12310,559 @@ - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - - - - - - - - - - - - - - - - - + - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - - - - + + - - + - - - - - - - - - - - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - - - - + + - - + - - - - - - - - - - - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - - - - + + - - + + - - - - - - - - - - - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + - + + + + + + + + - - - - - + file="src/numeral_to_display.vhd" line="31" + col="4" label="" delay_mechanism="inertial" + visible_flag="false" + guarded_target_state="unknown"> + + + - - + - - - + + + @@ -12658,593 +12870,116 @@ - - - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - - - - + + + + + + + + + + + + + + + + + + + - + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - + + + + + + + + + + + + + - - - + + + - - - - - - - - - - - - - - - - - - - + - + - - - + - - - - + + + - - + - - + + - + - - + + - - - + + + - + - + + - + - - - + + - - + - + - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + - - - - - - - - + + + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + - - - + + + - + - - - + - - - + + + - + - - - + - - + has_signal_flag="true" type_staticness="global"> + + - - + + + + - - + + - @@ -13614,3105 +13673,1129 @@ - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + - + + + + + + - + + + + - + + + + - - - - - - - - - - - - - + + + + - - - - - - - - - - - + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - + + + + + + - - - - - - - - - - - + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - + + + + + + - + + + + + + - - + + - + - + - - - + - - - + + - - - + - - - + - + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - + - + - - - + - - + - + - - - + - - - + + + - + - - - + - - - + + + - + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - - + + - - + + - - - - - + + + - - + + - - - + - - - + + + - - - - - + + + @@ -17009,166 +15090,164 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - - + + + - - + - - - + + + - - - + - - - + + + - - + - - - + + + - - - - - + + - - + + - - - - - + + + - - + + - - - + - - - + + + - - - - - + + + @@ -17179,1531 +15258,925 @@ - - + - - - + + + - - - - + + + - - + - - - + - - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + - - - - + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - + - + - + - - - + - - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - + - - - - - - - - - - - + + + + + + + + + + + + + + - - - - + + + + - - - - - - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - - - - - - + + + + + + + + + + + + + + + + + + + + - - + + + - - + + + + + + + - - + + - + - + - - - + + - - - + + - - - + + - - - + - + - - - - - - - - - - - - - - - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + + - + - - - + + - - - + + + - + - - - - - - - - - - - - - - - - - - + - - + has_signal_flag="true" type_staticness="local"> + + - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - @@ -18873,1579 +16717,1735 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + - - - + + - - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - + + + - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + - - + + - + - - + + + + + + + - - - - - - - - - - - - - - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + - - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - + - - - + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + - - + + + + + + + + + + - - - + + - - + + - - - - - + + + - - - - + + + - - - - - + + + - - - - + + + - - + + + + + - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - + + + - - - - - + + + - - - - + + + - - - - - + + + - - - - + + + - - - - - + + + - - - - + + + - - - - - - + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - + + + + + + + + + + + - + - - - - - - + + + + + + + + + + + + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - + - - - - - - - - - - - - - - - - + - - - + + + + + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + + + + + + + + + + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - + + + + + + + + + + + - - - + - - - - - - - - - - - - - + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + - + - + - + - - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - + - + - - + - - - + - + - - - + - - + - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - + + - - - - + + + - - + + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - + - - + @@ -22580,24 +20089,24 @@ - - - - + + + - - - - + + + + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - - + - - - + + + - + - - - - + + + - - - + - - + - - - + + + - - - + + - - - + + + - + - - - + - - + @@ -23038,24 +20547,24 @@ - - - - + + + - - - - + + + + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + + - - + - - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + - - - - - + + + - - - - + + + - - - + + + - - - - + + + - - - + + - - - + + + - + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - + + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - + - - - + - - - + + + - + - - - + @@ -24807,7 +22316,7 @@ - @@ -24818,7 +22327,7 @@ - @@ -24827,10 +22336,10 @@ - - + - - - + - - - + + + - + - - - + @@ -24876,7 +22385,7 @@ - @@ -24887,7 +22396,7 @@ - @@ -24896,10 +22405,10 @@ - - + - - - + - - - + + + - + - - - + @@ -24945,7 +22454,7 @@ - @@ -24956,7 +22465,7 @@ - @@ -24965,10 +22474,10 @@ - - - + + - - - + @@ -24998,19 +22507,19 @@ - - - - + + + - - - + + - - - + @@ -25040,19 +22549,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25125,19 +22634,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25338,19 +22847,19 @@ - - - - + + + - - - + + - - - + @@ -25380,19 +22889,19 @@ - - - - + + + - - - + + - - - + @@ -25422,19 +22931,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25592,19 +23101,19 @@ - - - - + + + - - - + + - - - + @@ -25634,19 +23143,19 @@ - - - - + + + - - - + + - - - + @@ -25676,19 +23185,19 @@ - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + - - - + + + - + - - - - + + + - - - + + - - - + @@ -25846,19 +23355,19 @@ - - - - + + + - - - + + - - - + @@ -25888,19 +23397,19 @@ - - - - + + + - - - + + - - - + @@ -25930,19 +23439,19 @@ - - - - + + + - - + - - - + - - - + + + - + - @@ -25983,10 +23492,10 @@ - - + - - - + - - - + + + - + - @@ -26027,10 +23536,10 @@ - - + - - - + - - - + + + - + - @@ -26070,10 +23579,10 @@ - - + - - - + - - - + + + - + - @@ -26113,10 +23622,10 @@ - - + - - - + - - - + + + - + - @@ -26157,190 +23666,188 @@ - - + + - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - + - - + - - - + - + - - + diff --git a/data/level/structural_level.lvl b/data/level/structural_level.lvl index 40aa455..dab377b 100644 --- a/data/level/structural_level.lvl +++ b/data/level/structural_level.lvl @@ -131,6 +131,9 @@ ;;;; String ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate string_matches string string) +;; is_accessed_by's signature must match is_read_element and +;; is_written_element's +(add_predicate is_accessed_by string process) ;;;; Type ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate is_approved_type type) diff --git a/data/property/cnes/CNE_01700.pro b/data/property/cnes/CNE_01700.pro index a0cb792..d254ad1 100644 --- a/data/property/cnes/CNE_01700.pro +++ b/data/property/cnes/CNE_01700.pro @@ -3,10 +3,46 @@ (x_re waveform CNE_01700_HAS_BAD_NAME) ) (and - (not (string_matches [identifier x_re] ".*_re")) + (not (string_matches [identifier [is_waveform_of x_re]] ".*_re")) (exists x waveform (exists x_r1 waveform (and + (exists ps2 process + (and + (is_in_sensitivity_list x_r1 ps2) + (is_in_sensitivity_list x ps2) + (is_accessed_by x_re ps2) + (CTL_verifies ps2 + (AF + (and + (expr_writes x_re) + (is_read_element "0" "and") + (or + (and + (is_read_structure "(?(??)?)") + (is_read_element "1" "not") + (is_read_element "2" x_r1) + (is_read_element "3" x) + ) + (and + (is_read_structure "(??(??))") + (is_read_element "1" x) + (is_read_element "2" "not") + (is_read_element "3" x_r1) + ) + ) + (AX + (not + (EF + (expr_writes x_r1) + ) + ) + ) + ) + ) + ) + ) + ) (exists ps1 process (and (is_accessed_by x_r1 ps1) @@ -28,7 +64,7 @@ (is_read_element "1" clk1) (EX (and - (has_option "COND_WAS_TRUE") + (has_option "cond_was_true") (does_not_reach_parent_before (and (expr_writes x_r1) @@ -99,42 +135,6 @@ ) ) ) - (exists ps2 process - (and - (is_in_sensitivity_list x_r1 ps2) - (is_in_sensitivity_list x ps2) - (is_accessed_by x_re ps2) - (CTL_verifies ps2 - (AF - (and - (expr_writes x_re) - (is_read_element "0" "and") - (or - (and - (is_read_structure "(?(??)?)") - (is_read_element "1" "not") - (is_read_element "2" x_r1) - (is_read_element "3" x) - ) - (and - (is_read_structure "(??(??))") - (is_read_element "1" x) - (is_read_element "2" "not") - (is_read_element "3" x_r1) - ) - ) - (AX - (not - (EF - (expr_writes x_r1) - ) - ) - ) - ) - ) - ) - ) - ) ) ) ) -- cgit v1.2.3-70-g09d2