-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #43 from tand00/main
SMC features for discrete verification
- Loading branch information
Showing
49 changed files
with
3,907 additions
and
122 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,65 @@ | ||
| #ifndef SMCQUERIES_H | ||
| #define SMCQUERIES_H | ||
|
|
||
| #include "AST.hpp" | ||
| #include <PQL/SMCExpressions.h> | ||
|
|
||
| namespace VerifyTAPN::AST { | ||
|
|
||
| struct SMCSettings { | ||
| int timeBound; | ||
| int stepBound; | ||
| float falsePositives; | ||
| float falseNegatives; | ||
| float indifferenceRegionUp; | ||
| float indifferenceRegionDown; | ||
| float confidence; | ||
| float estimationIntervalWidth; | ||
| bool compareToFloat; | ||
| float geqThan; | ||
|
|
||
| static SMCSettings fromPQL(unfoldtacpn::PQL::SMCSettings settings); | ||
| }; | ||
|
|
||
| class SMCQuery : public Query { | ||
| public: | ||
|
|
||
| SMCQuery(Quantifier quantifier, SMCSettings settings, Expression *expr) | ||
| : Query(quantifier, expr), smcSettings(settings) | ||
| { }; | ||
|
|
||
| SMCQuery(const SMCQuery &other) | ||
| : Query(other.quantifier, other.expr->clone()), smcSettings(other.smcSettings) | ||
| { }; | ||
|
|
||
| SMCQuery &operator=(const SMCQuery &other) { | ||
| if (&other != this) { | ||
| delete expr; | ||
| expr = other.expr->clone(); | ||
| smcSettings = other.smcSettings; | ||
| } | ||
| return *this; | ||
| } | ||
|
|
||
| virtual SMCQuery *clone() const; | ||
|
|
||
| void accept(Visitor &visitor, Result &context) override; | ||
|
|
||
|
|
||
| void setSMCSettings(SMCSettings newSettings) { | ||
| smcSettings = newSettings; | ||
| } | ||
|
|
||
| SMCSettings& getSmcSettings() { | ||
| return smcSettings; | ||
| } | ||
|
|
||
| private: | ||
| Quantifier quantifier; | ||
| Expression *expr; | ||
| SMCSettings smcSettings; | ||
| }; | ||
|
|
||
| } | ||
|
|
||
| #endif |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,117 @@ | ||
| #ifndef STOCHASTIC_STRUCTURE | ||
| #define STOCHASTIC_STRUCTURE | ||
|
|
||
| #include <random> | ||
| #include <sstream> | ||
| #include <string> | ||
|
|
||
| namespace VerifyTAPN::SMC { | ||
|
|
||
| enum FiringMode { | ||
| Oldest, | ||
| Youngest, | ||
| Random | ||
| }; | ||
|
|
||
| std::string firingModeName(FiringMode type); | ||
|
|
||
| enum DistributionType { | ||
| Constant, | ||
| Uniform, | ||
| Exponential, | ||
| Normal, | ||
| Gamma, | ||
| Erlang, | ||
| DiscreteUniform, | ||
| Geometric | ||
| }; | ||
|
|
||
| std::string distributionName(DistributionType type); | ||
|
|
||
| struct SMCUniformParameters { | ||
| double a; | ||
| double b; | ||
| }; | ||
| struct SMCExponentialParameters { | ||
| double rate; | ||
| }; | ||
| struct SMCNormalParameters { | ||
| double mean; | ||
| double stddev; | ||
| }; | ||
| struct SMCConstantParameters { | ||
| double value; | ||
| }; | ||
| struct SMCGammaParameters { | ||
| double shape; | ||
| double scale; | ||
| }; | ||
| struct SMCDiscreteUniformParameters { | ||
| int a; | ||
| int b; | ||
| }; | ||
| struct SMCGeometricParameters { | ||
| double p; | ||
| }; | ||
|
|
||
| union DistributionParameters { | ||
| SMCUniformParameters uniform; | ||
| SMCExponentialParameters exp; | ||
| SMCNormalParameters normal; | ||
| SMCConstantParameters constant; | ||
| SMCGammaParameters gamma; | ||
| SMCDiscreteUniformParameters discreteUniform; | ||
| SMCGeometricParameters geometric; | ||
| }; | ||
|
|
||
| struct Distribution { | ||
| DistributionType type; | ||
| DistributionParameters parameters; | ||
|
|
||
| template<typename T> | ||
| double sample(T& engine, const unsigned int precision = 0) const { | ||
| double date = 0; | ||
| switch(type) { | ||
| case Constant: | ||
| date = parameters.constant.value; | ||
| break; | ||
| case Uniform: | ||
| date = std::uniform_real_distribution(parameters.uniform.a, parameters.uniform.b)(engine); | ||
| break; | ||
| case Exponential: | ||
| date = std::exponential_distribution(parameters.exp.rate)(engine); | ||
| break; | ||
| case Normal: | ||
| date = std::normal_distribution(parameters.normal.mean, parameters.normal.stddev)(engine); | ||
| break; | ||
| case Gamma: | ||
| case Erlang: | ||
| date = std::gamma_distribution(parameters.gamma.shape, parameters.gamma.scale)(engine); | ||
| break; | ||
| case DiscreteUniform: | ||
| date = std::uniform_int_distribution(parameters.discreteUniform.a, parameters.discreteUniform.b)(engine); | ||
| break; | ||
| case Geometric: | ||
| date = std::geometric_distribution(parameters.geometric.p)(engine); | ||
| break; | ||
| } | ||
| if(precision > 0) { | ||
| double factor = pow(10.0, precision); | ||
| date = round(date * factor) / factor; | ||
| } | ||
| return std::max(date, 0.0); | ||
| } | ||
|
|
||
| static Distribution urgent(); | ||
|
|
||
| static Distribution defaultDistribution(); | ||
|
|
||
| static Distribution fromParams(int distrib_id, double param1, double param2); | ||
|
|
||
| std::string toXML() const; | ||
|
|
||
| }; | ||
|
|
||
| } | ||
|
|
||
| #endif |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.