Rule Set Classification #610

monsterkrampe · 2025-02-03T06:57:36Z

This PR will add membership checks for various syntactic (and some semantic) classes of rule sets. The implementation is done by @xR0xEr.
(This will still take some time and I am mainly creating this Draft PR now to have a place for review and discussion.)

…checks

… efficient) refactoring

…raphMap

… tests

monsterkrampe · 2025-02-03T06:59:48Z

nemo/Cargo.toml

@@ -54,6 +54,8 @@ bytecount = "0.6.8"
 colored = "2"

 [dev-dependencies]
+assert_cmd = "2.0"


I don't see why we would need assert_cmd.

It will be removed. I overlooked it somehow.

monsterkrampe · 2025-02-03T07:01:35Z

nemo/src/lib.rs

@@ -32,6 +32,8 @@ pub mod execution;
 pub mod rule_model;
 pub mod util;

+pub mod static_checks;


At some point, we should rename this as static_check is a bit too generic. Maybe something like ruleset_classification could work but I'm not quite sold on that either.

Right now, this module is implemented on data types of the rule_model module. Maybe rule_model_classification would be a good name? Also since it is based on the rule_model module, wouldn't it be better to make it a submodule of rule_model?

I think I would keep it separate. Maybe even have it in its own crate. These static analysis are useful but not required for anything happening in the Nemo Core so I rather see it as something that we put "on top". But this should be discussed in a bigger group. Some of the checks could potentially be used to influence the reasoning strategies...

monsterkrampe · 2025-02-03T07:05:08Z

nemo/src/rule_model/components/rule.rs

@@ -147,6 +147,24 @@ impl Rule {
        result
    }

+    pub fn positive_variables_as_vec(&self) -> Vec<&Variable> {


Would it make sense to return an iterator instead of a vector here?
Probably the above method returning a HashSet could then also be implemented based on the method returning the iterator.

Yes, it would make sense. I used it to get the join variables of a rule. Since same elements in a set is not possible, the other method was not sufficient. Maybe this can be added to the IterableVariables-Trait?

monsterkrampe · 2025-02-03T07:12:44Z

nemo/src/rule_model/origin.rs

@@ -5,7 +5,7 @@ use std::hash::Hash;
 pub(crate) type ExternalReference = usize;

 /// Origin of a program component
-#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
+#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash, Ord, PartialOrd)]


Is it really required that this is Ord and PartialOrd? I think the structs having Origin as one of their field have a custom implementation of Ord and PartialOrd anyway that does not involve comparing the origin at all.

monsterkrampe · 2025-02-03T07:16:05Z

nemo/src/static_checks/acyclicity_graph_constructor.rs

+    fn weak_acyclicity_graph(&'a self) -> WeakAcyclicityGraph<'a>;
+}
+
+impl<'a> AcyclicityGraphConstructor<'a> for RuleSet {


If only implemented on a RuleSet, the name of the trait is misleading. Also, why have the trait at all if its implementation is just calling JointAcyclicityGraph::build_graph? We could replace calls of the method joint_acyclicity_graph simply by directly calling JointAcyclicityGraph::build_graph.

I made this because build_graph method of JointAcyclicityGraph and WeakAcyclicityGraph looked pretty much the same. I hoped to refactor that into actually just one method but I couldn't do it myself. The idea was to give an input (in form of an enum) to decide whether the JointAcyclicityGraph or WeakAcyclicityGraph should be build.

monsterkrampe · 2025-02-03T08:10:30Z

nemo/tests/test.rs

+        Ok(program) => program,
+        Err((_program, report)) => {
+            report.eprint()?;
+            return Err(Box::new(Error::new(ErrorKind::Other, "error1")));


I think it is ok to now have error handling here and to just expect Ok from the Results since we run these checks on predefined rule sets, which should always succeed parsing.
(Same below.)

Will be done.

monsterkrampe · 2025-02-03T08:11:12Z

resources/testcases_static_checks/.DS_Store

Don't add MacOS specific stuff to git!
(Feel free to add .DS_Store to the root .gitignore.)

Sorry, I somehow forgot to add it.
Will be done.

monsterkrampe · 2025-02-03T08:19:14Z

resources/testcases_static_checks/tests/positive/.DS_Store

Remove mac stuff

monsterkrampe · 2025-02-03T08:32:04Z

nemo/src/static_checks/positions.rs

I think there is a lot to be reworked here.
For example, in general positions are independent of specific acyclicity checks so the code should be independent too, that is generic in places where MarkingType and AttackingType are currently hardcoded.
As for the acyclicity_graphs I do not really like the approach of introducing various traits on type aliases.
I think I need to play around with this a little bit to see what makes sense here...

I've done the playing around in acyclicity_graphs.rs. I think we can make similar adjustments here.

monsterkrampe · 2025-02-03T08:46:16Z

nemo/src/static_checks/rule_set.rs

I'll also play around here with possible refactorings.

I've done the playing around in acyclicity_graphs.rs. I think we can make similar adjustments here.

As you wrote in some comment above some things are unnecessary complicated. I agree on that. Some things can be written more easily and shouldn't need as much code as it does right now.
To be honest, I do not like every refactoring you have done in the last commit. For example, the new implementation of the new function of both graphs is written much shorter than before which is good. But I think it cannot be read as easy as before since both functions are quite big now.
Is there a way where we can find a compromise on that one?

mkroetzsch · 2025-02-04T08:01:05Z

General comment: It would be good to think about the API and UI for running these checks. I have created an issue #611 for this purpose.

…rn as we discussed. This reverts commit b1b64f9.

…s and use the Builder-Pattern. Also I reduced the number of traits significantly.

… of the construction of the special positions

…ed methods significantly. Reimplementing some methods for Variable as methods for RuleAndVariable

monsterkrampe

Looks nice overall. I left some specific comments again :)

monsterkrampe · 2025-03-12T07:12:31Z

nemo/src/static_checks/acyclicity_graphs.rs

+        special_edge_cycles
+    }
+
+    fn edge_is_special(&self, node: &Position<'a>, next_node: &Position<'a>) -> bool {


I think there is kind of a convention to have methods returning bool named as is_... or at least have them start with a verb (is, contains, ...). That is, I would go for is_edge_special here. (This reminds me of ruby's convention, where this method would probably be called edge_special?.)

monsterkrampe · 2025-03-12T07:16:55Z

nemo/src/static_checks/acyclicity_graphs.rs

+            .any(|cycle| self.cycle_contains_special_edge(cycle))
+    }
+
+    fn cycle_contains_special_edge(&self, cycle: &Cycle<Position<'a>>) -> bool {


Similar to the comment below, I think contains_special_edge_in_cycle would be a better name.

monsterkrampe · 2025-03-12T07:41:03Z

nemo/src/static_checks/positions.rs

+    }
+
+    /// Returns the common marking of a RuleSet.
+    pub fn build_and_check_marking(&self) -> Option<Positions> {


I think it would be good if the method names (at least for the public methods) would somehow indicate what this marking is for. I assume it's for the sticky check? Maybe also it would be worthwhile to rename occurrences of "Marking" to "StickyMarking" but I'm less sure about that...

monsterkrampe · 2025-03-12T07:51:40Z

nemo/src/static_checks/positions.rs

+    }
+}
+
+trait AffectedPositionsBuilderPrivate<'a> {


The capabilities described by this trait are not really a builder pattern.
Maybe I would call this trait AffectedPositionInference because both RuleSets and Rule are "capable" of infering affected positions (possibly based on already given positions).

monsterkrampe · 2025-03-12T07:52:32Z

nemo/src/static_checks/positions.rs

+    }
+}
+
+trait AttackedPositionsBuilderPrivate<'a> {


Same as above and the same also applies below.
Also keep in mind in general that traits do not describe entities but capabilities. (This a bit different from interface in object oriented languages I would say.)

monsterkrampe · 2025-03-12T07:55:43Z

nemo/src/static_checks/rule_set.rs

+pub struct RuleAndVariablePair<'a>(pub [RuleAndVariable<'a>; 2]);
+
+// NOTE: KEEP?
+/// This Trait provides methods to get all (HashSet<Position> / Positions) of some type.


To get rid of the Doc errors, I think you can put the code snippets in backticks (`).
For Example:

/// This Trait provides methods to get all (`HashSet<Position>` / `Positions`) of some type.

monsterkrampe · 2025-03-12T08:02:26Z

nemo/src/static_checks/rule_set.rs

+
+// NOTE: KEEP?
+/// This Trait provides methods to get all (HashSet<Position> / Positions) of some type.
+pub trait AllPositivePositions<'a> {


Just because a method is implemented on two different structures does not mean that there needs to be a trait for this.
For this trait and also others in this file I would say that the functionality is too specific to justify generalizing this into a trait.
If you want to keep the trait, it needs to describe a proper capability.

Also PositivePosition should be renamed to something like PositiveLiteralPosition because it is not clear what it means for a Position to be positive.

xR0xEr and others added 30 commits August 25, 2024 16:39

commiting before adding some code to rule.rs

ef65b0f

all checks written down + first implementations of some checks

c268d0c

some refactoring

8b0bc54

update commit: further refactoring and some implementing for guarded …

ea509cc

…checks

fully implemented function for getting positions of variable in a rule

79a5051

Merge branch 'main' into feature/static_checks

2769d47

fully integrated main branch into my new created files

c88f8b7

some refactoring and implementation of initial_affected_positions()

e8dfe9c

update commit and some refactoring

445a003

update commit

5b3dd1f

update commit: some refactoring and some implemantation

b59a0ce

Rewrite Positions subtract method

5510060

outsourced struct Positions in an own file

29f6a67

outsourced struct RuleSet into an own file, and some major (hopefully…

063ce25

… efficient) refactoring

update commit

ef0dc67

implemented concluding function to calculate the affected positions

61c3802

implemented marking check

ed59dda

implemented jointly guarded checks

45f6224

added shy check

9fb4af2

update commit

ecae4a0

started implementing DependencyGraph for more checks

73370eb

update commit for creating new branch positions_using_ref

ddb1b5e

added Ord implementation for Tag, so I can use Position as Node for G…

ea5e28f

…raphMap

fixed every error so far but it can be optimized

7fe9dbe

new error

95f6f4a

difference now takes a ref

253851b

update commit

5897665

update commit

b866160

some refactoring

b2483d6

finished implementation of acyclicity graphs

8e811ce

xR0xEr added 13 commits January 6, 2025 22:30

start of implementation for weakly_sticky check

6f007d5

refactoring how lukas wanted

50e57a2

refactor how lukas wanted it

304a01e

some easy refactoring

85af7d2

init commit

7c8f271

Merge branch 'main' into feature/static_checks

be989b3

Merge branch 'feature/static_checks' into test/static_checks

49eb764

reimplemented infinite_rank_positions because I somehow deleted it :(

5c60835

Merge branch 'feature/static_checks' into test/static_checks

0bdcfdd

implemented TestCase struct for static checks and implemented datalog…

219fae9

… tests

added some tests

8def53a

commiting before i try something

81da690

made all tests work

6a69f0d

monsterkrampe added the enhancement New feature or request label Feb 3, 2025

monsterkrampe self-assigned this Feb 3, 2025

monsterkrampe commented Feb 3, 2025

View reviewed changes

monsterkrampe added 2 commits February 3, 2025 10:32

Remove unnecessary acyclicity_graph_constructor

3246860

Refactor acyclicity_graphs.rs

b1b64f9

mkroetzsch mentioned this pull request Feb 4, 2025

API design for rule program analyses and/or transformations #611

Open

xR0xEr added 9 commits March 6, 2025 11:00

Revert "Refactor acyclicity_graphs.rs" to implement the Builder-Patte…

93e10ab

…rn as we discussed. This reverts commit b1b64f9.

refactored acyclicity_graphs.rs, so the graphs are now Wrapper-Struct…

682f6ae

…s and use the Builder-Pattern. Also I reduced the number of traits significantly.

Refactor rule_set.rs: First elimination of some types and traits

abae590

Refactor ruleset.rs: ended trait elimination

29f945d

Refactor: positions.rs: elimination of verbose traits and refactoring…

e15022a

… of the construction of the special positions

removed macOS specific .DS_Store

9507583

added type RuleAndVariable and refactored with it

cd399b9

major refactoring in the building of both graphs. Reduced and Optimis…

5d0e89a

…ed methods significantly. Reimplementing some methods for Variable as methods for RuleAndVariable

implemented method positive_variables_iter() for rule

a0f6dea

monsterkrampe commented Mar 12, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rule Set Classification #610

Rule Set Classification #610

monsterkrampe commented Feb 3, 2025

monsterkrampe Feb 3, 2025

xR0xEr Feb 4, 2025

monsterkrampe Feb 3, 2025

xR0xEr Feb 4, 2025

monsterkrampe Feb 6, 2025

monsterkrampe Feb 3, 2025

xR0xEr Feb 4, 2025

monsterkrampe Feb 3, 2025

monsterkrampe Feb 3, 2025

xR0xEr Feb 4, 2025

monsterkrampe Feb 3, 2025

xR0xEr Feb 4, 2025

monsterkrampe Feb 3, 2025

xR0xEr Feb 4, 2025

monsterkrampe Feb 3, 2025

monsterkrampe Feb 3, 2025

monsterkrampe Feb 3, 2025

monsterkrampe Feb 3, 2025

monsterkrampe Feb 3, 2025

xR0xEr Feb 4, 2025

mkroetzsch commented Feb 4, 2025

monsterkrampe left a comment

monsterkrampe Mar 12, 2025

monsterkrampe Mar 12, 2025

monsterkrampe Mar 12, 2025

monsterkrampe Mar 12, 2025

monsterkrampe Mar 12, 2025

monsterkrampe Mar 12, 2025

monsterkrampe Mar 12, 2025

Rule Set Classification #610

Are you sure you want to change the base?

Rule Set Classification #610

Conversation

monsterkrampe commented Feb 3, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mkroetzsch commented Feb 4, 2025

monsterkrampe left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment