Skip to content

Parameterized Priced Extension - #35

Draft
M4th942 wants to merge 15 commits into
UPPAALModelChecker:mainfrom
M4th942:Param.Cost.Opt.Reachability
Draft

Parameterized Priced Extension#35
M4th942 wants to merge 15 commits into
UPPAALModelChecker:mainfrom
M4th942:Param.Cost.Opt.Reachability

Conversation

@M4th942

@M4th942 M4th942 commented Aug 19, 2026

Copy link
Copy Markdown
  • create separate data structures
  • add tests
  • implement basic functions

@M4th942
M4th942 requested a review from mikucionisaau August 19, 2026 12:40
@M4th942
M4th942 marked this pull request as draft August 19, 2026 12:40
@CLAassistant

CLAassistant commented Aug 19, 2026

Copy link
Copy Markdown

CLA assistant check
All committers have signed the CLA.

Comment thread include/dbm/ParamPricedDBM.h Outdated
/**
* A parameter constraint is of the form (a_0 + sum^n_{i=1} a_i p_i) <= 0
*/
class ParameterConstraint { public: std::vector<int> coeffs; };

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
class ParameterConstraint { public: std::vector<int> coeffs; };
struct ParameterConstraint { std::vector<int> coeffs; };

Comment thread include/dbm/ParamPricedDBM.h Outdated
*/
class ParameterConstraint { public: std::vector<int> coeffs; };

class Polyhedron { public: std::vector<ParameterConstraint> constraints; };

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
class Polyhedron { public: std::vector<ParameterConstraint> constraints; };
struct Polyhedron { std::vector<ParameterConstraint> constraints; };

Comment thread include/dbm/ParamPricedDBM.h Outdated
Comment on lines +30 to +42
class DbmBound
{
public:
int value; // constant coeff of the constraint
bool strict; // is the constraint strict?

constexpr DbmBound(int value, bool strict): value(value), strict(strict){}
bool isInfinite() const { return value == INF; } // is this constraint unrestraining?
bool isLooserThan(const DbmBound& other) const {
return value > other.value || (value == other.value && strict && !other.strict);
}
DbmBound negate() const { assert(!isInfinite()); return DbmBound(-value, !strict); }
};

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
class DbmBound
{
public:
int value; // constant coeff of the constraint
bool strict; // is the constraint strict?
constexpr DbmBound(int value, bool strict): value(value), strict(strict){}
bool isInfinite() const { return value == INF; } // is this constraint unrestraining?
bool isLooserThan(const DbmBound& other) const {
return value > other.value || (value == other.value && strict && !other.strict);
}
DbmBound negate() const { assert(!isInfinite()); return DbmBound(-value, !strict); }
};
struct DbmBound
{
constexpr DbmBound(int value, bool strict): value(value), strict(strict){}
bool isInfinite() const { return value == INF; } // is this constraint unrestraining?
bool isLooserThan(const DbmBound& other) const {
return value > other.value || (value == other.value && strict && !other.strict);
}
DbmBound negate() const { assert(!isInfinite()); return DbmBound(-value, !strict); }
private:
int value; // constant coeff of the constraint
bool strict; // is the constraint strict?
};
struct DbmBound {
   int32_t& value() { return value; }
   const int32_t& value() const { return value; }
private:
    int32_t _value:31, _strict:1;
}

Comment thread include/dbm/ParamPricedDBM.h Outdated
Comment on lines +43 to +44
constexpr DbmBound INF_BOUND(INF,true);
constexpr DbmBound DIAG_BOUND(0,false);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
constexpr DbmBound INF_BOUND(INF,true);
constexpr DbmBound DIAG_BOUND(0,false);
constexpr auto INF_BOUND = DbmBound{INF,true};
constexpr auto DIAG_BOUND = DbmBound{0,false};

Comment thread include/dbm/ParamPricedDBM.h Outdated



constexpr int INF = INT_MAX >> 1;

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
constexpr int INF = INT_MAX >> 1;
constexpr auto INF = std::numeric_limits<int>::max() >> 1u;

Comment thread src/ParamPricedDBM.cpp Outdated
Comment on lines +14 to +25
/**
* constructs an unrestrained matrix
* @param dim
* @param param
*/
Ppdbm::Ppdbm(int dim, int param)
: dim(dim),
param(param),
DBM(dim),
offsetCost(param + 1),
rates(dim, std::vector<int>(param + 1))
{}

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

move it to header file (either inside class or outside with inline

Suggested change
/**
* constructs an unrestrained matrix
* @param dim
* @param param
*/
Ppdbm::Ppdbm(int dim, int param)
: dim(dim),
param(param),
DBM(dim),
offsetCost(param + 1),
rates(dim, std::vector<int>(param + 1))
{}
/**
* constructs an unrestrained matrix
* @param dim
* @param param
*/
Ppdbm::Ppdbm(int dim, int param)
: dim{dim},
param{param},
DBM{dim},
offsetCost(param + 1),
rates(dim, std::vector<int>(param + 1))
{}

Comment thread src/ParamPricedDBM.cpp Outdated
Comment on lines +32 to +35
std::fill(DBM.data.begin(), DBM.data.end(), INF_BOUND);
for (int i = 0; i < dim; ++i) {
DBM(i,i)= DIAG_BOUND;
}

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

move this to DBM as a separate method

Comment thread src/ParamPricedDBM.cpp Outdated

// The constraint empties the zone?
if (constraint.negate().isLooserThan(DBM(j, i))) {
DBM(i, j) = constraint;

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
DBM(i, j) = constraint;
DBM(i, j) = std::move(constraint);

Comment thread src/ParamPricedDBM.cpp Outdated
}

// Add the constraint and close the DBM
DBM(i, j) = constraint;

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
DBM(i, j) = constraint;
DBM(i, j) = std::move(constraint);

Comment thread src/ParamPricedDBM.cpp Outdated
@@ -0,0 +1,92 @@
/* -*- mode: C++; c-file-style: "stroustrup"; c-basic-offset: 4; indent-tabs-mode: nil; -*- */

#include "../include/dbm/ParamPricedDBM.h"

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
#include "../include/dbm/ParamPricedDBM.h"
#include "dbm/ParamPricedDBM.h"

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants