Integrate sin, cos and constants to Storm Jani parser #556

MarcoLm993 · 2024-05-27T11:38:17Z

This PR introduces support to the sin and cos operators, and to the PI and Euler number constants.

In particular, for the sin and cos operators I introduced a new expression type called trigonometric, that can be used later on in case other trigonometric operators will be integrated in storm.

Please let me know if I missed any additional place where the aforementioned operators need to be defined.

sjunges · 2024-05-27T12:52:16Z

src/storm-parsers/parser/JaniParser.cpp

@@ -1432,6 +1442,16 @@ storm::expressions::Expression JaniParser<ValueType>::parseExpression(Json const
                STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scope.description << ".");
            }
        }
+        if (expressionStructure.count("constant") == 1) {


Here, the expression now represents an approximation of the actual expression in the jani file. This is something to discuss a bit.

If I understand it correctly, you suggest to have something like this for PI (and the same for e):

if (constantStr == "π") { return storm::expressions::pi(); }

Did I get it right?

Hello,
I started looking into implementing this and I am not sure on what would be the preferred way to go.
My current understanding is that we need to have an additional class inherited from BaseExpression, that we can call ConstantValueExpression (or anything else), and this would provide an enum for the ConstantValue to store (i.e. PI and E), together with the same methods as for the RationalLiteralExpression class.

Taking this path means that some more boilerplate code needs to be written (for now I only found all the classes inherited from ExpressionVisitor, but maybe there is more), so I want to ask whether this is what you had in mind with your comment above, before I start implementing everything that is required.

@tquatmann your input would be greatly appreciated here

I personally would indeed tend to use a ConstantValueExpression or maybe a RealLiteralExpression?

What you describe is the most correct and most complete way to implement this. However, unless someone sees an important use case for π and e outside of jani models, I suggest to reduce the mentioned boilerplate code a bit:

Put your new expression class here, where we collect all expressions that are somewhat special for JANI. Given the current naming scheme, the new class should have suffix ...LiteralExpression, maybe TranscendentalNumberLiteralExpression ?

Extend the JaniExpressionVisitor and every class that inherits from this (fortunately, these are only a hand full and it's almost always clear what to do).

Extend the substituteConstantsInPlace function of the JANI model, so that it can (optionally, controlled by an argument) approximate transcendentalNumberLiterals. Apply this substitution, before building the model.

The advantage of this approach is that you can still export the parsed jani without approximating the constants.
For example, when using storm-conv --jani input.jani --constants N=4 --tojani output.jani, the constants should still be present.

Indeed, having the new ...LiteralExpression class in jani/expressions seems more appropriate for the current PR, thanks for your suggestion!

Hi @tquatmann ,

I just pushed a first attempt at integrating the TranscendentalNumberLiteralExpression in the JaniParser.
I am not sure this is 100% what you had in mind, since it resulted in an unexpected amount of changes around the code. Please let me know if there is anything that you think should be done differently.

Also, the unit tests and all the remaining comments will come at a later commit. This is just to make sure the changes related to this comment match your requests.

I just pushed some more changes I needed to do in order to have storm-conv working as you described.
Somehow this ended up touching an unexpected amount of files, I hope this is still fine with you, but of course I am open to any suggestion you might have.

In the next days I will address the last few comments you had (namely a missing type check and accepting integers as argument of trigonometric operators).

src/storm/storage/expressions/Expression.cpp

sjunges · 2024-05-27T13:00:49Z

Hi Marco,

great!

I think that it is debatable whether pi should be the same as 3.14.... I currently would argue that as an expression, it should be a function wihtout arguments (a symbol, that is) and only upon evaluating it, it should be interpreted with an approximation. @tquatmann @volkm
It would be good if you could add some small tests, i.e., a small programme with sin/cos and pi/e and show that this gets properly parsed.
We probably do not handle model building for jani models with these constructs. Thus, I guess that the Jani Builders should get methods that check whether these ingredients are in the jani model and refuse working with them. One approach here would be to use the model features of Jani. If trig is not added as a model feature, the parser should complain (or at least during a 'finalize' call) and the model builders should check whether this model feature is present. Let us know if you have any questions about this!

Best,
Sebastian

MarcoLm993 · 2024-05-27T13:14:06Z

Hi Sebastian,

thanks for the very quick feedback!

Point 1, I replied in the initial comment, I think i understand your point.
Point 2, I already have a small jani model to check that the new features are parsed correctly, I can add that in STORM, too, for the unit test!
Point 3, I think I understood your point, I will try to have a look and reach out in case of doubts!

Best,
Marco

tquatmann · 2024-06-05T09:12:23Z

src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp

+                case OperatorType::Cos:
+                case OperatorType::Sin:
+                    // The operands expect a real value. Raise an exception
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot apply cos or sin to an integer value.");


My understanding of the JANI-spec is that e.g. sin(10) would be valid in JANI as int is also a valid numeric type.

That is true. At the same time, the operator's output will always be a rational value, regardless of the input type. Anyway, I will add support for having integers as input.

Signed-off-by: Marco Lampacrescia <[email protected]>

…the model Signed-off-by: Marco Lampacrescia <[email protected]>

…nput type Signed-off-by: Marco Lampacrescia <[email protected]>

MarcoLm993 · 2024-06-12T13:18:04Z

Hello @sjunges and @tquatmann ,

I just pushed the last changes related to this PR. Now it should be good to go, if you do not spot anything else to change. :)

Looking forward to your inputs.

Best,
Marco

MarcoLm993 · 2024-06-12T13:22:28Z

src/storm/storage/jani/Model.cpp

    return *this;
 }

 Model Model::substituteConstants() const {
    Model result(*this);
    result.replaceUnassignedVariablesWithConstants();
-    result.substituteConstantsInPlace();
+    result.substituteConstantsInPlace(false);
    return result;
 }

 Model Model::substituteConstantsFunctions() const {


I added to this method the substitution of Transcendental numbers with Rational numbers, too.
Do you think it makes sense to reflect that in the name of the method, too? Something like substituteConstantsFunctionsTranscendentals?

Right now, it is a bit inconsistent that substituteConstants does not substitute transcendentals, while substituteConstantsFunctions does. Changing the name as you suggest sounds good to me.

Perfect, will do it!

sjunges · 2024-06-19T09:10:23Z

src/storm/generator/JaniNextStateGenerator.cpp

@@ -156,6 +158,7 @@ bool JaniNextStateGenerator<ValueType, StateType>::canHandle(storm::jani::Model
    features.remove(storm::jani::ModelFeature::DerivedOperators);
    features.remove(storm::jani::ModelFeature::Functions);  // can be substituted
    features.remove(storm::jani::ModelFeature::StateExitRewards);
+    features.remove(storm::jani::ModelFeature::TrigonometricFunctions);


Is this true? If so, I think this should be covered in a test.
If you are not sure, I would not allow this right now?

Hello Sebastian,

I am using it in the smc extension we are developing in the CONVINCE, so I am quite convinced this is working.
However, having one more test never hurts! :)

Some references about the smc use case:

test: https://github.com/convince-project/smc_storm/blob/main/test/test_models.cpp#L58

where this is used: https://github.com/convince-project/smc_storm/blob/main/src/model_checker/state_generation.cpp#L42

If you want to make sure that we dont break this, a test definitively does not hurt :-)

I adapted the test_trigonometry jani file to not expand forever and added a test for it in the ExplicitJaniModelBuilderTest gtest, (that is the only place I found with similar tests).
The new unit test can be found in this commit: 6b54f7c
On doing it, I found that transcendental numbers were not handled correctly in the constant variables bounds, but now they are handled, too.

sjunges · 2024-06-19T09:13:43Z

src/storm/storage/expressions/Type.h

@@ -187,7 +196,7 @@ class IntegerType : public BaseType {
    virtual bool isIntegerType() const override;

   private:
-    static const uint64_t mask = (1ull << 62);
+    static const uint64_t mask = (1ull << 58);


Is there a reason these have changed?

Yes, it was required for the type comparison here implemented here: to ensure that a transcendental number type is considered a non-integer number by the various model visitors, its mask must evaluate to a value higher than the one inn IntegerType.
Since in this implementation the mask is generated by setting a single bit in a uint64 variable, RationalType was getting the highest possible value, and IntegerType the one right before that. For this reason, I had to shift all of them to make space for the newly implemented TranscendentalNumberType.

Why is the shift decreased by 4 and not just by 1? My understanding is that masks (1ull << 61), (1ull << 62) and (1ull << 63) are now unused, correct?

When introducing the TranscendentalNumbers, I had to do the shift because I needed the related type mask value to be greater than the rational numbers one, that was using the highest possible value.
While implementing the shift, I thought that it would have been much easier to add the new mask if the last value wasn't already used up, and following that reasoning, I made sure that there were some unused values before and after the existing Type masks.

Functionality wise, this makes no difference, but it makes it easier to add new types in the future, if that will be ever needed.

Anyway, if you prefer to have it as it was before, I can make sure there are no unused values starting from the last one.

Thanks for clarifying. I just wanted to make sure that I didn't miss some detail concerning the unused masks.

sjunges · 2024-06-19T09:16:23Z

src/storm/storage/jani/TemplateEdgeDestination.cpp

-void TemplateEdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-    assignments.substitute(substitution);
+void TemplateEdgeDestination::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution,
+                                         bool const& substituteTranscendentalNumbers) {


bool by const& triggers a warning on my system

I can remove the reference. On my system quite some warning are triggered, so it is hard to notice new ones.
Are there more warnings that were added by this PR?

I had a look in the repository and bool const& seems to be a common pattern for function definitions in STORM.

Of course I can switch the ones I added to be bool const, by dropping the reference, but maybe it would make sense to make that consistent throughout the whole repository. The same could be done for all other basic types (int, float, double, char).

In case, I believe that should be tackled in a separated PR :)

I changed all declarations of bool const& substituteTranscendentalNumbers to not pass the value by reference anymore here: 6f016ca
On my machine, this seems not to throw warnings anymore.

sjunges · 2024-06-19T09:17:00Z

src/storm/storage/jani/TemplateEdge.cpp


    for (auto& assignment : assignments) {
-        assignment.substitute(substitution);
+        assignment.substitute(substitution, substituteTranscendentalNumbers);


is this maybe something that can be avoided by having a sensible default for this?

I am not sure, since this is set in the JaniModel's methods to substitute constants (around here) and must be propagated down to the various entries of the model. The value depends whether we want to preserve the transcendental numbers (e.g. storm-conv) or not (when we run the evaluation).
A way to not have the this argument would be to set a static variable for the jani visitor, to signal whether we want to substitute transcendental numbers or not, but I wouldn't recommend it, since it makes the code execution less clear.

Signed-off-by: Marco Lampacrescia <[email protected]>

tquatmann

Thanks for doing all this! 👍

There are some rather minor comments left. Apart from that, this is looking good!

I believe we could eventually replace all these substitute methods by a JaniTraverser but that is something for a different PR.

tquatmann · 2024-07-04T18:24:23Z

src/storm/storage/expressions/Type.h

@@ -187,7 +196,7 @@ class IntegerType : public BaseType {
    virtual bool isIntegerType() const override;

   private:
-    static const uint64_t mask = (1ull << 62);
+    static const uint64_t mask = (1ull << 58);


Why is the shift decreased by 4 and not just by 1? My understanding is that masks (1ull << 61), (1ull << 62) and (1ull << 63) are now unused, correct?

tquatmann · 2024-07-04T18:49:32Z

src/storm/storage/jani/Model.cpp

    return *this;
 }

 Model Model::substituteConstants() const {
    Model result(*this);
    result.replaceUnassignedVariablesWithConstants();
-    result.substituteConstantsInPlace();
+    result.substituteConstantsInPlace(false);
    return result;
 }

 Model Model::substituteConstantsFunctions() const {


Right now, it is a bit inconsistent that substituteConstants does not substitute transcendentals, while substituteConstantsFunctions does. Changing the name as you suggest sounds good to me.

tquatmann · 2024-07-04T18:59:07Z

src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp

@@ -60,7 +60,7 @@ std::shared_ptr<BaseExpression const> ConstructorArrayExpression::size() const {
 std::shared_ptr<BaseExpression const> ConstructorArrayExpression::at(uint64_t i) const {
    std::map<storm::expressions::Variable, storm::expressions::Expression> substitution;
    substitution.emplace(indexVar, this->getManager().integer(i));
-    return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution).getBaseExpressionPointer();
+    return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution, true).getBaseExpressionPointer();


Suggested change

return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution, true).getBaseExpressionPointer();

return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution, false).getBaseExpressionPointer();

If I see this correctly, one wouldn't want to substitute transcendentalNumbers at this point.

I think you are right, I am switching it to false in the upcoming commit!

tquatmann · 2024-07-04T19:04:34Z

src/storm/storage/jani/types/BoundedType.cpp

@@ -66,10 +66,10 @@ storm::expressions::Expression const& BoundedType::getUpperBound() const {
 void BoundedType::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {


Why does this not pass a bool substituteTranscendentalNumbers ?

If I remember correctly, I was just afraid of growing the amount of changes too large, but looking at that again, there is no reason to not have the substituteTranscendentalNumbers flag here as well. I will add that to the upcoming commit!

…bstitution method in JaniModel Signed-off-by: Marco Lampacrescia <[email protected]>

MarcoLm993

Hi, thanks for your review.
I addressed the comments from @tquatmann and pushed them in the last commit, and I added one comment about the bit shift for the Type maks.
Let me know what you think about it.

MarcoLm993 · 2024-07-08T08:14:37Z

src/storm/storage/expressions/Type.h

@@ -187,7 +196,7 @@ class IntegerType : public BaseType {
    virtual bool isIntegerType() const override;

   private:
-    static const uint64_t mask = (1ull << 62);
+    static const uint64_t mask = (1ull << 58);


When introducing the TranscendentalNumbers, I had to do the shift because I needed the related type mask value to be greater than the rational numbers one, that was using the highest possible value.
While implementing the shift, I thought that it would have been much easier to add the new mask if the last value wasn't already used up, and following that reasoning, I made sure that there were some unused values before and after the existing Type masks.

Functionality wise, this makes no difference, but it makes it easier to add new types in the future, if that will be ever needed.

Anyway, if you prefer to have it as it was before, I can make sure there are no unused values starting from the last one.

MarcoLm993 · 2024-07-08T08:36:15Z

src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp

@@ -60,7 +60,7 @@ std::shared_ptr<BaseExpression const> ConstructorArrayExpression::size() const {
 std::shared_ptr<BaseExpression const> ConstructorArrayExpression::at(uint64_t i) const {
    std::map<storm::expressions::Variable, storm::expressions::Expression> substitution;
    substitution.emplace(indexVar, this->getManager().integer(i));
-    return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution).getBaseExpressionPointer();
+    return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution, true).getBaseExpressionPointer();


I think you are right, I am switching it to false in the upcoming commit!

MarcoLm993 · 2024-07-08T08:40:02Z

src/storm/storage/jani/Model.cpp

    return *this;
 }

 Model Model::substituteConstants() const {
    Model result(*this);
    result.replaceUnassignedVariablesWithConstants();
-    result.substituteConstantsInPlace();
+    result.substituteConstantsInPlace(false);
    return result;
 }

 Model Model::substituteConstantsFunctions() const {


Perfect, will do it!

MarcoLm993 · 2024-07-08T08:46:18Z

src/storm/storage/jani/types/BoundedType.cpp

@@ -66,10 +66,10 @@ storm::expressions::Expression const& BoundedType::getUpperBound() const {
 void BoundedType::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {


If I remember correctly, I was just afraid of growing the amount of changes too large, but looking at that again, there is no reason to not have the substituteTranscendentalNumbers flag here as well. I will add that to the upcoming commit!

tquatmann

Thanks for looking into my comments. To me, this PR looks ready to be merged!

sjunges · 2024-07-13T17:37:53Z

Many thanks for all the work.

MarcoLm993 · 2024-07-15T07:24:49Z

I am the one thanking you for the discussions and for looking into this :)

MarcoLm993 force-pushed the support-for-sin-cos-constants branch from be3eeb3 to 77ad64e Compare May 27, 2024 11:58

sjunges reviewed May 27, 2024

View reviewed changes

src/storm/storage/expressions/Expression.cpp Show resolved Hide resolved

sjunges self-assigned this May 29, 2024

tquatmann reviewed Jun 5, 2024

View reviewed changes

MarcoLm993 added 2 commits June 10, 2024 14:45

Integrate sin, cos and constants to Storm Jani parser

a8d180a

Signed-off-by: Marco Lampacrescia <[email protected]>

Introduce TranscendentalNumberLiteralExpression and adapt JaniVisitors

6fb451b

Signed-off-by: Marco Lampacrescia <[email protected]>

MarcoLm993 force-pushed the support-for-sin-cos-constants branch from 77ad64e to 6fb451b Compare June 10, 2024 13:07

MarcoLm993 added 3 commits June 10, 2024 18:42

Add trigonometric-function feature and test jani model

f8ff8db

Signed-off-by: Marco Lampacrescia <[email protected]>

Adaptation to substitute transcendental numbers only when evaluating …

69e0eb3

…the model Signed-off-by: Marco Lampacrescia <[email protected]>

Support for integer input in trigonometric functions and checks for i…

af3337a

…nput type Signed-off-by: Marco Lampacrescia <[email protected]>

MarcoLm993 commented Jun 12, 2024

View reviewed changes

sjunges reviewed Jun 19, 2024

View reviewed changes

MarcoLm993 added 2 commits June 20, 2024 12:20

Make a bounded trigonometry test, to run that in a unit test

6b54f7c

Signed-off-by: Marco Lampacrescia <[email protected]>

Fix warning due to passing booleans by reference

6f016ca

Signed-off-by: Marco Lampacrescia <[email protected]>

tquatmann reviewed Jul 4, 2024

View reviewed changes

Make transcendentals substitution optional for JaniType and rename su…

c10bbbe

…bstitution method in JaniModel Signed-off-by: Marco Lampacrescia <[email protected]>

MarcoLm993 commented Jul 8, 2024

View reviewed changes

tquatmann approved these changes Jul 8, 2024

View reviewed changes

sjunges merged commit 7553a4a into moves-rwth:master Jul 13, 2024
15 checks passed

volkm added a commit to volkm/stormpy that referenced this pull request Jul 15, 2024

Adaption to changes in Storm (moves-rwth/storm#556)

465c871

volkm mentioned this pull request Jul 15, 2024

Adaption to changes in Storm moves-rwth/stormpy#174

Merged

	return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution, true).getBaseExpressionPointer();
	return storm::jani::substituteJaniExpression(elementExpression->toExpression(), substitution, false).getBaseExpressionPointer();

		@@ -66,10 +66,10 @@ storm::expressions::Expression const& BoundedType::getUpperBound() const {
		void BoundedType::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {

Integrate sin, cos and constants to Storm Jani parser #556

Integrate sin, cos and constants to Storm Jani parser #556

Conversation

MarcoLm993 commented May 27, 2024

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

sjunges commented May 27, 2024

MarcoLm993 commented May 27, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MarcoLm993 commented Jun 12, 2024

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

MarcoLm993 Jun 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MarcoLm993 Jun 19, 2024 • edited Loading

Choose a reason for hiding this comment

tquatmann left a comment • edited Loading

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

MarcoLm993 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

tquatmann left a comment

Choose a reason for hiding this comment

sjunges commented Jul 13, 2024

MarcoLm993 commented Jul 15, 2024

MarcoLm993 Jun 19, 2024 •

edited

Loading

MarcoLm993 Jun 19, 2024 •

edited

Loading

tquatmann left a comment •

edited

Loading