adjusted comment style and updated constant-folding example

Author: Laschoking

examples/constant-folding/constant-folding.rls

@@ -1,82 +1,82 @@
-% this simple implementation does NOT consider the control flow graph
-% i.e. if (){
-%           x=1;} 
-%       else{
-%           x=2;} 
-%       y=x; 
-% will lead to inconsistencies in the calculation
-% thus it is insufficient for real world examples
+@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
+false("false"^^xsd:boolean).
 
-% NOTE: AssignLocal MUST NOT contain phi-assignments, otherwise the chase is not successfull
-% run something like 'grep -v "phi-assign" data/AssignLocal.tsv.gz > data/AssignLocal.tsv.gz'
+%! this simple implementation does NOT consider the control flow graph
+%! e.g. if (){
+%!           x=1;} 
+%!       else{
+%!           x=2;} 
+%!       y=x; 
+%! will lead to inconsistencies in the calculation
+%! thus it is insufficient for real world examples
 
-% dive into doop-syntax:
-% the instrucion-id (?ins) is a unique identifier for each line of intermediate code (IR)
-% everything that happens on one IR-line, will be linked with the same instruction-id
-% it may look like this: "<Example: void main(java.lang.String[])>/assign/4"
-% where "<Example: void main(java.lang.String[])>/" is the function signature
-% "assign/" means it is an assignment (i.e. a=b;), and "4" is the line number of the statement
+%! dive into doop-syntax:
+%! the instrucion-id (?ins) is a unique identifier for each line of intermediate code (IR)
+%! everything that happens on one IR-line, will be linked with the same instruction-id
+%! it may look like this: "<Example: void main(java.lang.String[])>/assign/4"
+%! where "<Example: void main(java.lang.String[])>/" is the function signature
+%! "assign/" means it is an assignment (i.e. a=b;), and "4" is the line number of the statement
 
 
-%loaded files from doop:
+%% load facts generated by doop
 
-% AssignNumConstant:        contains all variables that hold a constant value (i.e. a = 1) -> this is the base for this analysis
+%%% Contains all variables that hold a constant value (i.e. a = 1) -> this is the base for this analysis
 @import AssignNumConstant :- tsv { resource = "data/AssignNumConstant.tsv.gz" } .
 
 
-% AssignLocal:              holds assignments of type a = b. 
-% which only holds static assignments (assignments that include the string "phi-assign" are dynamically and have been removed)
+%%% Holds assignments of type a = b. 
+%%% Which only holds static assignments (assignments that include the string "phi-assign" are dynamically and have been removed)
 @import AssignLocal :- tsv { resource = "data/AssignLocal.tsv.gz" } .
 
 
-% OperatorAt:               links an instruction-id of a unary or binary expression to its operator
-%                           most common operators: (~, +, -, *, /, >=, <=, ==, <<, !=, >, len, <, %, ^, cmp, &, cmpl, cmpg, >>>, >>, |)
+%%% Links an instruction-id of a unary or binary expression to its operator
+%%% Most common operators: (~, +, -, *, /, >=, <=, ==, <<, !=, >, len, <, %, ^, cmp, &, cmpl, cmpg, >>>, >>, |)
 @import OperatorAt :- tsv { resource = "data/OperatorAt.tsv.gz" } .
 
 
-% AssignUnop:               holds the instruction-id and variable that is getting assigned by a unary expression
+%%% Holds the instruction-id and variable that is getting assigned by a unary expression
 @import AssignUnop :- tsv { resource = "data/AssignUnop.tsv.gz" } .
 
 
-% AssignBinop:              holds the instruction-id and the variable that is getting assigned by a binary expression
+%%% Holds the instruction-id and the variable that is getting assigned by a binary expression
 @import AssignBinop :- tsv { resource = "data/AssignBinop.tsv.gz" } .
 
 
-% AssignOperFrom:           links an instruction-id of a unary or binary expression, to the VARIABLE(S) that are used    
-%                           (i.e. a = b + c, will have two entries in AssignOperFrom)
+%%% Links an instruction-id of a unary or binary expression, to the VARIABLE(S) that are used    
+%%% (e.g. a = b + c, will have two entries in AssignOperFrom)
 @import AssignOperFrom :- tsv { resource = "data/AssignOperFrom.tsv.gz" } .
 
 
-% AssignOperFromConstant:   links an instruction-id of a unary or binary expression to the CONSTANT(S) used 
-%                           (i.e. a = b + 2, will have one entries in AssignOperFromConstant)
+%%% Links an instruction-id of a unary or binary expression to the CONSTANT(S) used 
+%%% (e.g. a = b + 2, will have one entry in AssignOperFromConstant)
 @import AssignOperFromConstant :- tsv { resource = "data/AssignOperFromConstant.tsv.gz" }.
 
 
-
-% Implementation:
+%% Implementation:
 % IntegerConstant contains all constants (given & computed)
 % it is initialized with all constants that are supplied by doop in AssignNumConstant (i.e. a = 2;)
 % ConstFolding will contain all variables and values where constant folding & propagation was successfull
+
 % the doop relations AssignUnop & AssignBinop ONLY contain the instruction-id and the assigned variable 
 % -> we need to manually check, if the expression consists of constants (a =  1 + 2;) variables (a = b + c;) or both (a = b + 2;)
 %   -> 2 cases for unary expressions:   (- const), (- var)                           
 %   -> 3 cases each for binary expressions (+,*): (var + var), (const + const), (const + var)-> order of var & const is irrelevant
 %   -> 4 cases each for binary expressions (-, /): (var - var), (const - const), (const - var), (var - const) -> order of var & const is relevant 
 
-
-% Initialize IntegerConstant with all constants from AssignNumConstant
+%%% Initialize IntegerConstant with all constants from AssignNumConstant
 IntegerConstant(?var, ?val,?meth) :-
     AssignNumConstant(_, _, ?val, ?var, ?meth).
 
- %Assignment without Operator (i.e.  a  = b)
+%%% Assignment without Operator (i.e.  a  = b)
+%%% Remove statements containing 'phi-assign' since they indicate CFG-issues
 IntegerConstant(?var_to, ?val, ?meth),
 ConstFolding(?ins,?var_to, ?val,  ?meth) :-
     AssignLocal(?ins, _, ?var_from, ?var_to, ?meth),
-        IntegerConstant(?var_from, ?val, ?meth).
-
+    false(CONTAINS(?ins,"phi-assign")),
+    IntegerConstant(?var_from, ?val, ?meth).
 
 
-% Unary-Negation: "-" is translated to "~" in OperatorAt
+%% Unary-Negation: "-" is translated to "~" in OperatorAt
 
 IntegerConstant(?var, 0 - ?val1, ?meth),
 ConstFolding(?ins,?var, 0 - ?val1,  ?meth) :-
@@ -94,7 +94,8 @@ ConstFolding(?ins,?var, 0 - ?val1,  ?meth) :-
     AssignOperFromConstant(?ins, _, ?val1).
 
 
-% Addition
+%% Addition
+
 IntegerConstant(?var, ?val1 + ?val2, ?meth),
 ConstFolding(?ins,?var, ?val1 + ?val2,  ?meth) :-
     AssignBinop(?ins,_, ?var, ?meth),
@@ -127,7 +128,7 @@ ConstFolding(?ins,?var, ?val1 + ?val2,  ?meth) :-
 
 
 
-% Subtraction
+%% Subtraction
 
 IntegerConstant(?var, ?val1 - ?val2, ?meth),
 ConstFolding(?ins,?var, ?val1 - ?val2,  ?meth) :-
@@ -170,8 +171,7 @@ ConstFolding(?ins,?var, ?val1 - ?val2,  ?meth) :-
     IntegerConstant(?var2, ?val2,?meth).
 
 
-
-% Multiplication
+%% Multiplication
 
 IntegerConstant(?var, ?val1 * ?val2, ?meth),
 ConstFolding(?ins,?var, ?val1 * ?val2,  ?meth) :-
@@ -202,7 +202,8 @@ ConstFolding(?ins,?var, ?val1 * ?val2,  ?meth) :-
     IntegerConstant(?var1, ?val1, ?meth),
     IntegerConstant(?var2, ?val2,?meth).
 
-% Division
+
+%% Division
 
 IntegerConstant(?var, ?val1 / ?val2, ?meth),
 ConstFolding(?ins,?var, ?val1 / ?val2,  ?meth) :-

examples/datalogMtlSensor/datalogMtlSensor.rls

@@ -1,6 +1,6 @@
-%%% Sensor Readings Example from https://datalogmtl.github.io/
+%! Sensor Readings Example from https://datalogmtl.github.io/
 
-%% Facts
+% Original facts:
 % HighTemperature(sensor1)@[0,27.5]
 % HighTemperature(sensor2)@3.5
 % HighTemperature(sensor2)@5.1
@@ -9,14 +9,16 @@
 % HighTemperature(sensor2)@20
 % SameLocation(sensor1,sensor2)@(-inf,+inf)
 
-%% Rules
+% Original Rules:
 % Overheat(X) :- ALWAYS[-10,0] HighTemperature(X)
 % Overheat(X) :- ALWAYS[-20,0] SOMETIME[-5.5,0] HighTemperature(X)
 % Alert :- Overheat(X), Overheat(Y), SameLocation(X,Y)
-
-%% Entailment check
+% Entailment check
 % Alert@25
 
+
+%% Translated facts
+
 HighTemperature("sensor1", 0.0, 27.5).
 HighTemperature("sensor2", 3.5, 3.5).
 HighTemperature("sensor2", 5.1, 5.1).
@@ -25,7 +27,10 @@ HighTemperature("sensor2", 14.7, 14.7).
 HighTemperature("sensor2", 20.0, 20.0).
 SameLocation("sensor1", "sensor2"). % Always holds
 
-% aux rule to combine intervals
+
+%% Translated rules 
+
+%%% aux rule to combine intervals
 HighTemperatureSometimes(?Sensor, ?StartA, ?EndB) :- 
     HighTemperatureSometimes(?Sensor, ?StartA, ?EndA),
     HighTemperatureSometimes(?Sensor, ?StartB, ?EndB),
@@ -34,7 +39,7 @@ HighTemperatureSometimes(?Sensor, ?StartA, ?EndB) :-
     ?StartA <= ?StartB,
     ?EndA <= ?EndB.
 
-% aux rule to combine intervals
+%%% aux rule to combine intervals
 Overheat(?Sensor, ?StartA, ?EndB) :- 
     Overheat(?Sensor, ?StartA, ?EndA),
     Overheat(?Sensor, ?StartB, ?EndB),
@@ -43,26 +48,28 @@ Overheat(?Sensor, ?StartA, ?EndB) :-
     ?StartA <= ?StartB,
     ?EndA <= ?EndB.
 
-% rule 1
+%%% corresponds to rule 1
 Overheat(?Sensor, ?Start + 10.0, ?End) :- 
     HighTemperature(?Sensor, ?Start, ?End), 
     ?End - ?Start >= 10.0.
 
-% rule 2 (split into two rules)
+
+%% corresponds to rule 2 (split into two rules)
+
 HighTemperatureSometimes(?Sensor, ?Start, ?End + 5.5) :- 
     HighTemperature(?Sensor, ?Start, ?End).
 Overheat(?Sensor, ?Start + 20.0, ?End) :- 
     HighTemperatureSometimes(?Sensor, ?Start, ?End), 
     ?End - ?Start >= 20.0.
 
-% rule 3 (slightly altered since we do not have nullary predicates)
+%%% corresponds to rule  3 (slightly altered since we do not have nullary predicates)
 Alert(?SensorA, MAX(?StartA, ?StartB), MIN(?EndA, ?EndB)), Alert(?SensorB, MAX(?StartA, ?StartB), MIN(?EndA, ?EndB)) :- 
     Overheat(?SensorA, ?StartA, ?EndA), 
     Overheat(?SensorB, ?StartB, ?EndB), 
     SameLocation(?SensorA, ?SensorB),
     ?StartA <= ?EndB,
     ?StartB <= ?EndA.
 
-@output Overheat.
-@output Alert.
+@export Overheat :- tsv{resource="Overheat.tsv"}.
+@export Alert :- tsv{resource="Alert.tsv"}.
 

examples/datalogMtlWeather/datalogMtlWeather.rls

@@ -1,14 +1,7 @@
-%%% Inspired by:
-%%% https://github.com/wdimmy/MeTeoR/blob/main/experiments/AAAI2022/programs/w.txt
-%%% (diamondminus in head should really be a boxminus according to original example; seems to be a typo in the meteor repo)
+%! Inspired by:
+%! https://github.com/wdimmy/MeTeoR/blob/main/experiments/AAAI2022/programs/w.txt
+%! (diamondminus in head should really be a boxminus according to original example; seems to be a typo in the meteor repo)
 
-%% (a)
-%% Boxminus[0,1]ExcessiveHeat(X):-Diamondminus[0,1]TempAbove41(X),Boxminus[0,1]TempAbove24(X)
-%% HeatAffectedState(X):-ExcessiveHeat(Y),LocatedInState(Y,X)
-%%
-%% (b)
-%% Boxminus[0,1]HeavyWind(X):-Boxminus[0,1]HeavyWindForce(X)
-%% HeavyWindAffectedState(X):-HeavyWind(Y),LocatedInState(Y,X)
 
 %% Weather Station in Ohio with some Temperature Data
 
@@ -20,49 +13,52 @@ HeavyWindForce("StationA", 113.4,115.2).
 HeavyWindForce("StationA", 115.3,117.0).
 HeavyWindForce("StationA", 117.1,118.0).
 
-%% (a)
+%% Boxminus[0,1]ExcessiveHeat(X):-Diamondminus[0,1]TempAbove41(X),Boxminus[0,1]TempAbove24(X)
+%% HeatAffectedState(X):-ExcessiveHeat(Y),LocatedInState(Y,X)
 
-% diamondminus part of first body
+%%% diamondminus part of first body
 TempAbove41DiamondMinus1(?Station, ?Start, ?End + 1.0) 
     :- TempAbove41(?Station, ?Start, ?End).
-% boxminus part of first body 
+
+%%% boxminus part of first body 
 TempConstantOver24AtLeastFor1(?Station, ?Start + 1.0, ?End)
     :- TempAbove24(?Station, ?Start, ?End), 
         ?Start + 1.0 < ?End.
 
-% first rule using aux predicates
+%%% first rule using aux predicates
 ExcessiveHeat(?Station, MAX(?Start24, ?Start41) - 1.0, MIN(?End41, ?End24)) 
     :-  TempAbove41DiamondMinus1(?Station, ?Start41, ?End41),
         TempConstantOver24AtLeastFor1(?Station, ?Start24, ?End24),
         ?Start41 < ?End24,
         ?Start24 < ?End41.
 
-% second rule
+%%% second rule
 HeatAffectedState(?State, MAX(?StartHeat, ?StartIn), MIN(?EndHeat, ?EndIn)) 
     :-  ExcessiveHeat(?Station, ?StartHeat, ?EndHeat),
         LocatedInState(?Station, ?State, ?StartIn, ?EndIn),
         ?StartHeat < ?EndIn,
         ?StartIn < ?EndHeat.
 
-%% (b)
 
-% third rule
+%% Boxminus[0,1]HeavyWind(X):-Boxminus[0,1]HeavyWindForce(X)
+%% HeavyWindAffectedState(X):-HeavyWind(Y),LocatedInState(Y,X)
+
+%%% third rule
 HeavyWind(?Station, ?Start, ?End) 
     :-  HeavyWindForce(?Station, ?Start, ?End), 
         ?Start + 1.0 < ?End.
 
-% fourth rule
+%%% fourth rule
 HeavyWindAffectedState(?State, MAX(?StartWind, ?StartIn), MIN(?EndWind, ?EndIn))
     :-  HeavyWind(?Station, ?StartWind, ?EndWind),
         LocatedInState(?Station, ?State, ?StartIn, ?EndIn),
         ?StartWind < ?EndIn,
         ?StartIn < ?EndWind.
 
-@output TempAbove41DiamondMinus1.
-@output TempConstantOver24AtLeastFor1.
-@output ExcessiveHeat.
-@output HeatAffectedState.
-
-@output HeavyWind.
-@output HeavyWindAffectedState.
+@export TempAbove41DiamondMinus1 :- tsv{resource="TempAbove41DiamondMinus1.tsv"}.
+@export TempConstantOver24AtLeastFor1 :- tsv{resource="TempConstantOver24AtLeastFor1.tsv"}.
+@export ExcessiveHeat :- tsv{resource="ExcessiveHeat.tsv"}.
+@export HeatAffectedState :- tsv{resource="HeatAffectedState.tsv"}.
+@export HeavyWind :- tsv{resource="HeavyWind.tsv"}.
+@export HeavyWindAffectedState :- tsv{resource="HeavyWindAffectedState.tsv"}.
 

examples/lime-trees/old-lime-trees.rls

@@ -1,13 +1,16 @@
-%%% This example finds trees of (some species of lime/linden tree) in Dresden,
-%%% which are more than 200 years old.
-%%% 
-%%% It shows how to load (typed) data from (compressed) CSV files, how to
-%%% perform a recursive reachability query, and how to use datatype built-in to
-%%% find old trees. It can be modified to use a different species or genus of
-%%% plant, and by changing the required age.
+%! This example finds trees of (some species of lime/linden tree) in Dresden,
+%! which are more than 200 years old.
+%! 
+%! It shows how to load (typed) data from (compressed) CSV files, how to
+%! perform a recursive reachability query, and how to use datatype built-in to
+%! find old trees. It can be modified to use a different species or genus of
+%! plant, and by changing the required age.
 
-@import tree :- csv { resource = "dresden-trees-ages-heights.csv" } .    % location URL, species, age, height in m
-@import taxon :- csv { resource = "wikidata-taxon-name-parent.csv.gz" } . % Wikidata ID, taxon name, Wikidata ID of parent taxon
+%%% tree contains: (location URL, species, age, height in m)
+@import tree :- csv { resource = "dresden-trees-ages-heights.csv",format=(string,string,int,int)} .    
+
+%%% taxon contains: (Wikidata ID, taxon name, Wikidata ID of parent taxon)
+@import taxon :- csv { resource = "wikidata-taxon-name-parent.csv.gz" } . 
 
 limeSpecies(?X, Tilia) :- taxon(?X, Tilia, ?P).
 limeSpecies(?X, ?Name) :- taxon(?X, ?Name, ?Y), limeSpecies(?Y, ?N).