sjunges
11 years ago
59 changed files with 1737 additions and 130 deletions
-
3CMakeLists.txt
-
9resources/3rdparty/cudd-2.5.0/CMakeLists.txt
-
1resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
-
19resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c
-
65resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c
-
16resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
-
5resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh
-
2resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp
-
2resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp
-
2src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
-
2src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
2src/parser/PrctlParser.cpp
-
42src/parser/PrismParser.cpp
-
9src/parser/PrismParser.h
-
75src/storage/dd/CuddDd.cpp
-
68src/storage/dd/CuddDd.h
-
161src/storage/dd/CuddDdForwardIterator.cpp
-
130src/storage/dd/CuddDdForwardIterator.h
-
39src/storage/dd/CuddDdManager.cpp
-
21src/storage/dd/CuddDdManager.h
-
13src/storage/dd/DdForwardIterator.h
-
15src/storage/dd/DdMetaVariable.cpp
-
25src/storage/dd/DdMetaVariable.h
-
5src/storage/expressions/BinaryBooleanFunctionExpression.cpp
-
2src/storage/expressions/BinaryBooleanFunctionExpression.h
-
28src/storage/expressions/Expression.cpp
-
29src/storage/expressions/Expression.h
-
37src/storage/expressions/IdentifierSubstitutionVisitor.cpp
-
6src/storage/expressions/IdentifierSubstitutionVisitor.h
-
11src/storage/expressions/SimpleValuation.cpp
-
5src/storage/expressions/SimpleValuation.h
-
37src/storage/expressions/SubstitutionVisitor.cpp
-
6src/storage/expressions/SubstitutionVisitor.h
-
2src/storage/prism/Assignment.cpp
-
2src/storage/prism/BooleanVariable.cpp
-
2src/storage/prism/Command.cpp
-
5src/storage/prism/Constant.cpp
-
2src/storage/prism/Formula.cpp
-
2src/storage/prism/IntegerVariable.cpp
-
2src/storage/prism/Label.cpp
-
1src/storage/prism/LocatedInformation.h
-
4src/storage/prism/Program.cpp
-
2src/storage/prism/StateReward.cpp
-
2src/storage/prism/TransitionReward.cpp
-
2src/storage/prism/Update.cpp
-
2src/storage/prism/Variable.cpp
-
2test/functional/parser/PrismParserTest.cpp
-
60test/functional/parser/prism/coin2.nm
-
69test/functional/parser/prism/crowds5_5.pm
-
130test/functional/parser/prism/csma2_2.nm
-
24test/functional/parser/prism/die.pm
-
170test/functional/parser/prism/firewire.nm
-
96test/functional/parser/prism/leader3.nm
-
85test/functional/parser/prism/leader3_5.pm
-
40test/functional/parser/prism/two_dice.nm
-
219test/functional/parser/prism/wlan0_collide.nm
-
2test/functional/solver/GmmxxLinearEquationSolverTest.cpp
-
39test/functional/storage/CuddDdTest.cpp
-
9test/functional/storage/ExpressionTest.cpp
@ -0,0 +1,161 @@ |
|||
#include "src/storage/dd/CuddDdForwardIterator.h"
|
|||
#include "src/storage/dd/CuddDdManager.h"
|
|||
#include "src/storage/dd/DdMetaVariable.h"
|
|||
#include "src/exceptions/ExceptionMacros.h"
|
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { |
|||
// If the given generator is not yet at its end, we need to create the current valuation from the cube from
|
|||
// scratch.
|
|||
if (!this->isAtEnd) { |
|||
// Start by registering all meta variables in the valuation with the appropriate type.
|
|||
for (auto const& metaVariableName : *this->metaVariables) { |
|||
auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); |
|||
switch (metaVariable.getType()) { |
|||
case DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool: currentValuation.addBooleanIdentifier(metaVariableName); break; |
|||
case DdMetaVariable<DdType::CUDD>::MetaVariableType::Int: currentValuation.addIntegerIdentifier(metaVariableName); break; |
|||
} |
|||
} |
|||
|
|||
// And then get ready for treating the first cube.
|
|||
this->treatNewCube(); |
|||
} |
|||
} |
|||
|
|||
DdForwardIterator<DdType::CUDD>::DdForwardIterator(DdForwardIterator<DdType::CUDD>&& other) : ddManager(other.ddManager), generator(other.generator), cube(other.cube), value(other.value), isAtEnd(other.isAtEnd), metaVariables(other.metaVariables), cubeCounter(other.cubeCounter), relevantDontCareDdVariables(other.relevantDontCareDdVariables), currentValuation(other.currentValuation) { |
|||
// Null-out the pointers of which we took possession.
|
|||
other.cube = nullptr; |
|||
other.generator = nullptr; |
|||
} |
|||
|
|||
DdForwardIterator<DdType::CUDD>& DdForwardIterator<DdType::CUDD>::operator=(DdForwardIterator<DdType::CUDD>&& other) { |
|||
if (this != &other) { |
|||
this->ddManager = other.ddManager; |
|||
this->generator = other.generator; |
|||
this->cube = other.cube; |
|||
this->value = other.value; |
|||
this->isAtEnd = other.isAtEnd; |
|||
this->metaVariables = other.metaVariables; |
|||
this->cubeCounter = other.cubeCounter; |
|||
this->relevantDontCareDdVariables = other.relevantDontCareDdVariables; |
|||
this->currentValuation = other.currentValuation; |
|||
|
|||
// Null-out the pointers of which we took possession.
|
|||
other.cube = nullptr; |
|||
other.generator = nullptr; |
|||
} |
|||
return *this; |
|||
} |
|||
|
|||
DdForwardIterator<DdType::CUDD>::~DdForwardIterator() { |
|||
if (this->cube != nullptr) { |
|||
free(this->cube); |
|||
} |
|||
if (this->generator != nullptr) { |
|||
free(this->generator); |
|||
} |
|||
} |
|||
|
|||
DdForwardIterator<DdType::CUDD>& DdForwardIterator<DdType::CUDD>::operator++() { |
|||
LOG_ASSERT(!this->isAtEnd, "Illegally incrementing iterator that is already at its end."); |
|||
|
|||
// If there were no (relevant) don't cares or we have enumerated all combination, we need to eliminate the
|
|||
// found solutions and get the next "first" cube.
|
|||
if (this->relevantDontCareDdVariables.empty() || this->cubeCounter >= std::pow(2, this->relevantDontCareDdVariables.size()) - 1) { |
|||
// Get the next cube and check for emptiness.
|
|||
ABDD::NextCube(generator, &cube, &value); |
|||
this->isAtEnd = Cudd_IsGenEmpty(generator); |
|||
|
|||
// In case we are not done yet, we get ready to treat the next cube.
|
|||
if (!this->isAtEnd) { |
|||
this->treatNewCube(); |
|||
} |
|||
} else { |
|||
// Treat the next solution of the cube.
|
|||
this->treatNextInCube(); |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
void DdForwardIterator<DdType::CUDD>::treatNextInCube() { |
|||
// Start by increasing the counter and check which bits we need to set/unset in the new valuation.
|
|||
++this->cubeCounter; |
|||
|
|||
for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) { |
|||
auto const& metaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index])); |
|||
if (metaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) { |
|||
if ((this->cubeCounter & (1ull << index)) != 0) { |
|||
currentValuation.setBooleanValue(metaVariable.getName(), true); |
|||
} else { |
|||
currentValuation.setBooleanValue(metaVariable.getName(), false); |
|||
} |
|||
} else { |
|||
if ((this->cubeCounter & (1ull << index)) != 0) { |
|||
currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); |
|||
} else { |
|||
currentValuation.setIntegerValue(metaVariable.getName(), ((currentValuation.getIntegerValue(metaVariable.getName()) - metaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + metaVariable.getLow()); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
void DdForwardIterator<DdType::CUDD>::treatNewCube() { |
|||
this->relevantDontCareDdVariables.clear(); |
|||
|
|||
// Now loop through the bits of all meta variables and check whether they need to be set, not set or are
|
|||
// don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete
|
|||
// valuations later.
|
|||
for (auto const& metaVariableName : *this->metaVariables) { |
|||
auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName); |
|||
if (metaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) { |
|||
if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) { |
|||
currentValuation.setBooleanValue(metaVariableName, false); |
|||
} else if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) { |
|||
currentValuation.setBooleanValue(metaVariableName, true); |
|||
} else { |
|||
relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0)); |
|||
} |
|||
} else { |
|||
int_fast64_t intValue = 0; |
|||
for (uint_fast64_t bitIndex = 0; bitIndex < metaVariable.getNumberOfDdVariables(); ++bitIndex) { |
|||
if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) { |
|||
// Leave bit unset.
|
|||
} else if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) { |
|||
intValue |= 1ull << (metaVariable.getNumberOfDdVariables() - bitIndex - 1); |
|||
} else { |
|||
// Temporarily leave bit unset so we can iterate trough the other option later.
|
|||
// Add the bit to the relevant don't care bits.
|
|||
this->relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1)); |
|||
} |
|||
} |
|||
currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow()); |
|||
} |
|||
} |
|||
|
|||
// Finally, reset the cube counter.
|
|||
this->cubeCounter = 0; |
|||
} |
|||
|
|||
bool DdForwardIterator<DdType::CUDD>::operator==(DdForwardIterator<DdType::CUDD> const& other) const { |
|||
if (this->isAtEnd && other.isAtEnd) { |
|||
return true; |
|||
} else { |
|||
return this->ddManager.get() == other.ddManager.get() && this->generator == other.generator |
|||
&& this->cube == other.cube && this->value == other.value && this->isAtEnd == other.isAtEnd |
|||
&& this->metaVariables == other.metaVariables && this->cubeCounter == other.cubeCounter |
|||
&& this->relevantDontCareDdVariables == other.relevantDontCareDdVariables |
|||
&& this->currentValuation == other.currentValuation; |
|||
} |
|||
} |
|||
|
|||
bool DdForwardIterator<DdType::CUDD>::operator!=(DdForwardIterator<DdType::CUDD> const& other) const { |
|||
return !(*this == other); |
|||
} |
|||
|
|||
std::pair<storm::expressions::SimpleValuation, double> DdForwardIterator<DdType::CUDD>::operator*() const { |
|||
return std::make_pair(currentValuation, value); |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,130 @@ |
|||
#ifndef STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ |
|||
#define STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ |
|||
|
|||
#include <memory> |
|||
#include <cstdint> |
|||
#include <set> |
|||
#include <tuple> |
|||
#include <utility> |
|||
|
|||
#include "src/storage/dd/DdForwardIterator.h" |
|||
#include "src/storage/expressions/SimpleValuation.h" |
|||
|
|||
// Include the C++-interface of CUDD. |
|||
#include "cuddObj.hh" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
// Forward-declare the DdManager class. |
|||
template<DdType Type> class DdManager; |
|||
template<DdType Type> class Dd; |
|||
|
|||
template<> |
|||
class DdForwardIterator<DdType::CUDD> { |
|||
public: |
|||
friend class Dd<DdType::CUDD>; |
|||
|
|||
// Default-instantiate the constructor. |
|||
DdForwardIterator() = default; |
|||
|
|||
// Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then. |
|||
DdForwardIterator(DdForwardIterator<DdType::CUDD> const& other) = delete; |
|||
DdForwardIterator& operator=(DdForwardIterator<DdType::CUDD> const& other) = delete; |
|||
|
|||
// Provide move-construction and move-assignment, though. |
|||
DdForwardIterator(DdForwardIterator<DdType::CUDD>&& other); |
|||
DdForwardIterator& operator=(DdForwardIterator<DdType::CUDD>&& other); |
|||
|
|||
/*! |
|||
* Destroys the forward iterator and frees the generator as well as the cube if they are not the nullptr. |
|||
*/ |
|||
~DdForwardIterator(); |
|||
|
|||
/*! |
|||
* Moves the iterator one position forward. |
|||
*/ |
|||
DdForwardIterator<DdType::CUDD>& operator++(); |
|||
|
|||
/*! |
|||
* Returns a pair consisting of a valuation of meta variables and the value to which this valuation is |
|||
* mapped. Note that the result is returned by value. |
|||
* |
|||
* @return A pair of a valuation and the function value. |
|||
*/ |
|||
std::pair<storm::expressions::SimpleValuation, double> operator*() const; |
|||
|
|||
/*! |
|||
* Compares the iterator with the given one. Two iterators are considered equal when all their underlying |
|||
* data members are the same or they both are at their end. |
|||
* |
|||
* @param other The iterator with which to compare. |
|||
* @return True if the two iterators are considered equal. |
|||
*/ |
|||
bool operator==(DdForwardIterator<DdType::CUDD> const& other) const; |
|||
|
|||
/*! |
|||
* Compares the iterator with the given one. Two iterators are considered unequal iff they are not |
|||
* considered equal. |
|||
* |
|||
* @param other The iterator with which to compare. |
|||
* @return True if the two iterators are considered unequal. |
|||
*/ |
|||
bool operator!=(DdForwardIterator<DdType::CUDD> const& other) const; |
|||
|
|||
private: |
|||
/*! |
|||
* Constructs a forward iterator using the given generator with the given set of relevant meta variables. |
|||
* |
|||
* @param ddManager The manager responsible for the DD over which to iterate. |
|||
* @param generator The generator used to enumerate the cubes of the DD. |
|||
* @param cube The cube as represented by CUDD. |
|||
* @param value The value the cube is mapped to. |
|||
* @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any |
|||
* more. |
|||
* @param metaVariables The meta variables that appear in the DD. |
|||
*/ |
|||
DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables = nullptr); |
|||
|
|||
/*! |
|||
* Recreates the internal information when a new cube needs to be treated. |
|||
*/ |
|||
void treatNewCube(); |
|||
|
|||
/*! |
|||
* Updates the internal information when the next solution of the current cube needs to be treated. |
|||
*/ |
|||
void treatNextInCube(); |
|||
|
|||
// The manager responsible for the meta variables (and therefore the underlying DD). |
|||
std::shared_ptr<DdManager<DdType::CUDD>> ddManager; |
|||
|
|||
// The CUDD generator used to enumerate the cubes of the DD. |
|||
DdGen* generator; |
|||
|
|||
// The currently considered cube of the DD. |
|||
int* cube; |
|||
|
|||
// The function value of the current cube. |
|||
double value; |
|||
|
|||
// A flag that indicates whether the iterator is at its end and may not be moved further. This is also used |
|||
// for the check against the end iterator. |
|||
bool isAtEnd; |
|||
|
|||
// The set of meta variables appearing in the DD. |
|||
std::set<std::string> const* metaVariables; |
|||
|
|||
// A number that represents how many assignments of the current cube have already been returned previously. |
|||
// This is needed, because cubes may represent many assignments (if they have don't care variables). |
|||
uint_fast64_t cubeCounter; |
|||
|
|||
// A vector of tuples of the form <variable, metaVariableName, bitIndex>. |
|||
std::vector<std::tuple<ADD, std::string, uint_fast64_t>> relevantDontCareDdVariables; |
|||
|
|||
// The current valuation of meta variables. |
|||
storm::expressions::SimpleValuation currentValuation; |
|||
}; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_CUDDDDFORWARDITERATOR_H_ */ |
|||
@ -0,0 +1,13 @@ |
|||
#ifndef STORM_STORAGE_DD_DDFORWARDITERATOR_H_ |
|||
#define STORM_STORAGE_DD_DDFORWARDITERATOR_H_ |
|||
|
|||
#include "src/storage/dd/DdType.h" |
|||
|
|||
namespace storm { |
|||
namespace dd { |
|||
// Declare DdIterator class so we can then specialize it for the different DD types. |
|||
template<DdType Type> class DdForwardIterator; |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_STORAGE_DD_DDFORWARDITERATOR_H_ */ |
|||
@ -0,0 +1,60 @@ |
|||
// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] |
|||
// gxn/dxp 20/11/00 |
|||
|
|||
mdp |
|||
|
|||
// constants |
|||
const int N=2; |
|||
const int K; |
|||
const int range = 2*(K+1)*N; |
|||
const int counter_init = (K+1)*N; |
|||
const int left = N; |
|||
const int right = 2*(K+1)*N - N; |
|||
|
|||
// shared coin |
|||
global counter : [0..range] init counter_init; |
|||
|
|||
module process1 |
|||
|
|||
// program counter |
|||
pc1 : [0..3]; |
|||
// 0 - flip |
|||
// 1 - write |
|||
// 2 - check |
|||
// 3 - finished |
|||
|
|||
// local coin |
|||
coin1 : [0..1]; |
|||
|
|||
// flip coin |
|||
[] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1); |
|||
// write tails -1 (reset coin to add regularity) |
|||
[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); |
|||
// write heads +1 (reset coin to add regularity) |
|||
[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); |
|||
// check |
|||
// decide tails |
|||
[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); |
|||
// decide heads |
|||
[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); |
|||
// flip again |
|||
[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); |
|||
// loop (all loop together when done) |
|||
[done] (pc1=3) -> 1 : (pc1'=3); |
|||
|
|||
endmodule |
|||
|
|||
// construct remaining processes through renaming |
|||
module process2 = process1[pc1=pc2,coin1=coin2] endmodule |
|||
|
|||
// labels |
|||
label "finished" = pc1=3 & pc2=3 ; |
|||
label "all_coins_equal_0" = coin1=0 & coin2=0 ; |
|||
label "all_coins_equal_1" = coin1=1 & coin2=1 ; |
|||
label "agree" = coin1=coin2 ; |
|||
|
|||
// rewards |
|||
rewards "steps" |
|||
true : 1; |
|||
endrewards |
|||
|
|||
@ -0,0 +1,69 @@ |
|||
dtmc |
|||
|
|||
// probability of forwarding |
|||
const double PF = 0.8; |
|||
const double notPF = .2; // must be 1-PF |
|||
// probability that a crowd member is bad |
|||
const double badC = .167; |
|||
// probability that a crowd member is good |
|||
const double goodC = 0.833; |
|||
// Total number of protocol runs to analyze |
|||
const int TotalRuns = 5; |
|||
// size of the crowd |
|||
const int CrowdSize = 5; |
|||
|
|||
module crowds |
|||
// protocol phase |
|||
phase: [0..4] init 0; |
|||
|
|||
// crowd member good (or bad) |
|||
good: bool init false; |
|||
|
|||
// number of protocol runs |
|||
runCount: [0..TotalRuns] init 0; |
|||
|
|||
// observe_i is the number of times the attacker observed crowd member i |
|||
observe0: [0..TotalRuns] init 0; |
|||
|
|||
observe1: [0..TotalRuns] init 0; |
|||
|
|||
observe2: [0..TotalRuns] init 0; |
|||
|
|||
observe3: [0..TotalRuns] init 0; |
|||
|
|||
observe4: [0..TotalRuns] init 0; |
|||
|
|||
// the last seen crowd member |
|||
lastSeen: [0..CrowdSize - 1] init 0; |
|||
|
|||
// get the protocol started |
|||
[] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); |
|||
|
|||
// decide whether crowd member is good or bad according to given probabilities |
|||
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); |
|||
|
|||
// if the current member is a good member, update the last seen index (chosen uniformly) |
|||
[] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); |
|||
|
|||
// if the current member is a bad member, record the most recently seen index |
|||
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); |
|||
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); |
|||
|
|||
// good crowd members forward with probability PF and deliver otherwise |
|||
[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); |
|||
|
|||
// deliver the message and start over |
|||
[] phase=4 -> 1: (phase'=0); |
|||
|
|||
endmodule |
|||
|
|||
label "observe0Greater1" = observe0>1; |
|||
label "observe1Greater1" = observe1>1; |
|||
label "observe2Greater1" = observe2>1; |
|||
label "observe3Greater1" = observe3>1; |
|||
label "observe4Greater1" = observe4>1; |
|||
label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; |
|||
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; |
|||
@ -0,0 +1,130 @@ |
|||
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
|||
// gxn/dxp 04/12/01 |
|||
|
|||
mdp |
|||
|
|||
// note made changes since cannot have strict inequalities |
|||
// in digital clocks approach and suppose a station only sends one message |
|||
|
|||
// simplified parameters scaled |
|||
const int sigma=1; // time for messages to propagate along the bus |
|||
const int lambda=30; // time to send a message |
|||
|
|||
// actual parameters |
|||
const int N = 2; // number of processes |
|||
const int K = 2; // exponential backoff limit |
|||
const int slot = 2*sigma; // length of slot |
|||
// const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
|||
const int M = 3 ; // max number of slots to wait |
|||
//const int lambda=782; |
|||
//const int sigma=26; |
|||
|
|||
// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); |
|||
// formula min_collisions = min(cd1,cd2); |
|||
// formula max_collisions = max(cd1,cd2); |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// the bus |
|||
module bus |
|||
|
|||
b : [0..2]; |
|||
// b=0 - idle |
|||
// b=1 - active |
|||
// b=2 - collision |
|||
|
|||
// clocks of bus |
|||
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
|||
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
|||
|
|||
// a sender sends (ok - no other message being sent) |
|||
[send1] (b=0) -> (b'=1); |
|||
[send2] (b=0) -> (b'=1); |
|||
|
|||
// a sender sends (bus busy - collision) |
|||
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
|
|||
// finish sending |
|||
[end1] (b=1) -> (b'=0) & (y1'=0); |
|||
[end2] (b=1) -> (b'=0) & (y1'=0); |
|||
|
|||
// bus busy |
|||
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
|
|||
// collision detected |
|||
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
|||
|
|||
// time passage |
|||
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
|||
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
|||
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// model of first sender |
|||
module station1 |
|||
|
|||
// LOCAL STATE |
|||
s1 : [0..5]; |
|||
// s1=0 - initial state |
|||
// s1=1 - transmit |
|||
// s1=2 - collision (set backoff) |
|||
// s1=3 - wait (bus busy) |
|||
// s1=4 - successfully sent |
|||
|
|||
// LOCAL CLOCK |
|||
x1 : [0..max(lambda,slot)]; |
|||
|
|||
// BACKOFF COUNTER (number of slots to wait) |
|||
bc1 : [0..M]; |
|||
|
|||
// COLLISION COUNTER |
|||
cd1 : [0..K]; |
|||
|
|||
// start sending |
|||
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
|||
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
|||
|
|||
// transmitting |
|||
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
|||
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
|||
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
|||
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
|||
|
|||
// set backoff (no time can pass in this state) |
|||
// probability depends on which transmission this is (cd1) |
|||
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
|||
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
|||
|
|||
// wait until backoff counter reaches 0 then send again |
|||
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
|||
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
|||
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
|||
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
|||
|
|||
// once finished nothing matters |
|||
[time] (s1>=4) -> (x1'=0); |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// construct further stations through renaming |
|||
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// reward structure for expected time |
|||
rewards "time" |
|||
[time] true : 1; |
|||
endrewards |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// labels/formulae |
|||
label "all_delivered" = s1=4&s2=4; |
|||
label "one_delivered" = s1=4|s2=4; |
|||
label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); |
|||
|
|||
@ -0,0 +1,24 @@ |
|||
// Knuth's model of a fair die using only fair coins |
|||
dtmc |
|||
|
|||
module die |
|||
|
|||
// local state |
|||
s : [0..7] init 0; |
|||
// value of the dice |
|||
d : [0..6] init 0; |
|||
|
|||
[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); |
|||
[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); |
|||
[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); |
|||
[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); |
|||
[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); |
|||
[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); |
|||
[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); |
|||
[] s=7 -> 1: (s'=7); |
|||
|
|||
endmodule |
|||
|
|||
rewards "coin_flips" |
|||
[] s<7 : 1; |
|||
endrewards |
|||
@ -0,0 +1,170 @@ |
|||
// firewire protocol with integer semantics |
|||
// dxp/gxn 14/06/01 |
|||
|
|||
// CLOCKS |
|||
// x1 (x2) clock for node1 (node2) |
|||
// y1 and y2 (z1 and z2) clocks for wire12 (wire21) |
|||
mdp |
|||
|
|||
// maximum and minimum delays |
|||
// fast |
|||
const int rc_fast_max = 85; |
|||
const int rc_fast_min = 76; |
|||
// slow |
|||
const int rc_slow_max = 167; |
|||
const int rc_slow_min = 159; |
|||
// delay caused by the wire length |
|||
const int delay; |
|||
// probability of choosing fast |
|||
const double fast; |
|||
const double slow=1-fast; |
|||
|
|||
module wire12 |
|||
|
|||
// local state |
|||
w12 : [0..9]; |
|||
// 0 - empty |
|||
// 1 - rec_req |
|||
// 2 - rec_req_ack |
|||
// 3 - rec_ack |
|||
// 4 - rec_ack_idle |
|||
// 5 - rec_idle |
|||
// 6 - rec_idle_req |
|||
// 7 - rec_ack_req |
|||
// 8 - rec_req_idle |
|||
// 9 - rec_idle_ack |
|||
|
|||
// clock for wire12 |
|||
y1 : [0..delay+1]; |
|||
y2 : [0..delay+1]; |
|||
|
|||
// empty |
|||
// do not need y1 and y2 to increase as always reset when this state is left |
|||
// similarly can reset y1 and y2 when we re-enter this state |
|||
[snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0); |
|||
[snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0); |
|||
[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0); |
|||
[time] w12=0 -> (w12'=w12); |
|||
// rec_req |
|||
[snd_req12] w12=1 -> (w12'=1); |
|||
[rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0); |
|||
[snd_ack12] w12=1 -> (w12'=2) & (y2'=0); |
|||
[snd_idle12] w12=1 -> (w12'=8) & (y2'=0); |
|||
[time] w12=1 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_req_ack |
|||
[snd_ack12] w12=2 -> (w12'=2); |
|||
[rec_req12] w12=2 -> (w12'=3); |
|||
[time] w12=2 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_ack |
|||
[snd_ack12] w12=3 -> (w12'=3); |
|||
[rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0); |
|||
[snd_idle12] w12=3 -> (w12'=4) & (y2'=0); |
|||
[snd_req12] w12=3 -> (w12'=7) & (y2'=0); |
|||
[time] w12=3 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_ack_idle |
|||
[snd_idle12] w12=4 -> (w12'=4); |
|||
[rec_ack12] w12=4 -> (w12'=5); |
|||
[time] w12=4 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_idle |
|||
[snd_idle12] w12=5 -> (w12'=5); |
|||
[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0); |
|||
[snd_req12] w12=5 -> (w12'=6) & (y2'=0); |
|||
[snd_ack12] w12=5 -> (w12'=9) & (y2'=0); |
|||
[time] w12=5 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_idle_req |
|||
[snd_req12] w12=6 -> (w12'=6); |
|||
[rec_idle12] w12=6 -> (w12'=1); |
|||
[time] w12=6 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_ack_req |
|||
[snd_req12] w12=7 -> (w12'=7); |
|||
[rec_ack12] w12=7 -> (w12'=1); |
|||
[time] w12=7 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_req_idle |
|||
[snd_idle12] w12=8 -> (w12'=8); |
|||
[rec_req12] w12=8 -> (w12'=5); |
|||
[time] w12=8 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
// rec_idle_ack |
|||
[snd_ack12] w12=9 -> (w12'=9); |
|||
[rec_idle12] w12=9 -> (w12'=3); |
|||
[time] w12=9 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); |
|||
|
|||
endmodule |
|||
|
|||
module node1 |
|||
|
|||
// clock for node1 |
|||
x1 : [0..168]; |
|||
|
|||
// local state |
|||
s1 : [0..8]; |
|||
// 0 - root contention |
|||
// 1 - rec_idle |
|||
// 2 - rec_req_fast |
|||
// 3 - rec_req_slow |
|||
// 4 - rec_idle_fast |
|||
// 5 - rec_idle_slow |
|||
// 6 - snd_req |
|||
// 7- almost_root |
|||
// 8 - almost_child |
|||
|
|||
// added resets to x1 when not considered again until after rest |
|||
// removed root and child (using almost root and almost child) |
|||
|
|||
// root contention immediate state) |
|||
[snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0); |
|||
[rec_idle21] s1=0 -> (s1'=1); |
|||
// rec_idle immediate state) |
|||
[snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (s1'=5) & (x1'=0); |
|||
[rec_req21] s1=1 -> (s1'=0); |
|||
// rec_req_fast |
|||
[rec_idle21] s1=2 -> (s1'=4); |
|||
[snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0); |
|||
[time] s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168)); |
|||
// rec_req_slow |
|||
[rec_idle21] s1=3 -> (s1'=5); |
|||
[snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0); |
|||
[time] s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168)); |
|||
// rec_idle_fast |
|||
[rec_req21] s1=4 -> (s1'=2); |
|||
[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0); |
|||
[time] s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168)); |
|||
// rec_idle_slow |
|||
[rec_req21] s1=5 -> (s1'=3); |
|||
[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0); |
|||
[time] s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168)); |
|||
// snd_req |
|||
// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 |
|||
// also can set x1 to 0 upon entering this state |
|||
[rec_req21] s1=6 -> (s1'=0); |
|||
[rec_ack21] s1=6 -> (s1'=8); |
|||
[time] s1=6 -> (s1'=s1); |
|||
// almost root (immediate) |
|||
// loop in final states to remove deadlock |
|||
[] s1=7 & s2=8 -> (s1'=s1); |
|||
[] s1=8 & s2=7 -> (s1'=s1); |
|||
[time] s1=7 -> (s1'=s1); |
|||
[time] s1=8 -> (s1'=s1); |
|||
|
|||
endmodule |
|||
|
|||
// construct remaining automata through renaming |
|||
module wire21=wire12[w12=w21, y1=z1, y2=z2, |
|||
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, |
|||
rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] |
|||
endmodule |
|||
module node2=node1[s1=s2, s2=s1, x1=x2, |
|||
rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, |
|||
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] |
|||
endmodule |
|||
|
|||
// reward structures |
|||
// time |
|||
rewards "time" |
|||
[time] true : 1; |
|||
endrewards |
|||
// time nodes sending |
|||
rewards "time_sending" |
|||
[time] (w12>0 | w21>0) : 1; |
|||
endrewards |
|||
|
|||
label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)); |
|||
@ -0,0 +1,96 @@ |
|||
// asynchronous leader election |
|||
// 4 processes |
|||
// gxn/dxp 29/01/01 |
|||
|
|||
mdp |
|||
|
|||
const int N = 3; // number of processes |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
module process1 |
|||
|
|||
// COUNTER |
|||
c1 : [0..3-1]; |
|||
|
|||
// STATES |
|||
s1 : [0..4]; |
|||
// 0 make choice |
|||
// 1 have not received neighbours choice |
|||
// 2 active |
|||
// 3 inactive |
|||
// 4 leader |
|||
|
|||
// PREFERENCE |
|||
p1 : [0..1]; |
|||
|
|||
// VARIABLES FOR SENDING AND RECEIVING |
|||
receive1 : [0..2]; |
|||
// not received anything |
|||
// received choice |
|||
// received counter |
|||
sent1 : [0..2]; |
|||
// not send anything |
|||
// sent choice |
|||
// sent counter |
|||
|
|||
// pick value |
|||
[] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); |
|||
|
|||
// send preference |
|||
[p12] (s1=1) & (sent1=0) -> (sent1'=1); |
|||
// receive preference |
|||
// stay active |
|||
[p31] (s1=1) & (receive1=0) & !( (p1=0) & (p3=1) ) -> (s1'=2) & (receive1'=1); |
|||
// become inactive |
|||
[p31] (s1=1) & (receive1=0) & (p1=0) & (p3=1) -> (s1'=3) & (receive1'=1); |
|||
|
|||
// send preference (can now reset preference) |
|||
[p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); |
|||
// send counter (already sent preference) |
|||
// not received counter yet |
|||
[c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); |
|||
// received counter (pick again) |
|||
[c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
|||
|
|||
// receive counter and not sent yet (note in this case do not pass it on as will send own counter) |
|||
[c31] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); |
|||
// receive counter and sent counter |
|||
// only active process (decide) |
|||
[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
|||
// other active process (pick again) |
|||
[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3<N-1) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
|||
|
|||
// send preference (must have received preference) and can now reset |
|||
[p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); |
|||
// send counter (must have received counter first) and can now reset |
|||
[c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); |
|||
|
|||
// receive preference |
|||
[p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1); |
|||
// receive counter |
|||
[c31] (s1=3) & (receive1=1) & (c3<N-1) -> (c1'=c3+1) & (receive1'=2); |
|||
|
|||
// done |
|||
[done] (s1=4) -> (s1'=s1); |
|||
// add loop for processes who are inactive |
|||
[done] (s1=3) -> (s1'=s1); |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// construct further stations through renaming |
|||
module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule |
|||
module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// reward - expected number of rounds (equals the number of times a process receives a counter) |
|||
rewards "name" |
|||
[c12] true : 1; |
|||
endrewards |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0); |
|||
label "elected" = s1=4|s2=4|s3=4; |
|||
|
|||
@ -0,0 +1,85 @@ |
|||
// synchronous leader election protocol (itai & Rodeh) |
|||
// dxp/gxn 25/01/01 |
|||
|
|||
dtmc |
|||
|
|||
// CONSTANTS |
|||
const int N = 3; // number of processes |
|||
const int K = 5; // range of probabilistic choice |
|||
|
|||
// counter module used to count the number of processes that have been read |
|||
// and to know when a process has decided |
|||
module counter |
|||
|
|||
// counter (c=i means process j reading process (i-1)+j next) |
|||
c : [1..N-1]; |
|||
|
|||
// reading |
|||
[read] c<N-1 -> 1:(c'=c+1); |
|||
// finished reading |
|||
[read] c=N-1 -> 1:(c'=c); |
|||
//decide |
|||
[done] u1|u2|u3 -> 1:(c'=c); |
|||
// pick again reset counter |
|||
[retry] !(u1|u2|u3) -> 1:(c'=1); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> 1:(c'=c); |
|||
|
|||
endmodule |
|||
|
|||
// processes form a ring and suppose: |
|||
// process 1 reads process 2 |
|||
// process 2 reads process 3 |
|||
// process 3 reads process 1 |
|||
module process1 |
|||
|
|||
// local state |
|||
s1 : [0..3]; |
|||
// s1=0 make random choice |
|||
// s1=1 reading |
|||
// s1=2 deciding |
|||
// s1=3 finished |
|||
|
|||
// has a unique id so far (initially true) |
|||
u1 : bool; |
|||
|
|||
// value to be sent to next process in the ring (initially sets this to its own value) |
|||
v1 : [0..K-1]; |
|||
|
|||
// random choice |
|||
p1 : [0..K-1]; |
|||
|
|||
// pick value |
|||
[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) |
|||
+ 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); |
|||
// read |
|||
[read] s1=1 & u1 & c<N-1 -> 1:(u1'=(p1!=v2)) & (v1'=v2); |
|||
[read] s1=1 & !u1 & c<N-1 -> 1:(u1'=false) & (v1'=v2) & (p1'=0); |
|||
// read and move to decide |
|||
[read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); |
|||
[read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0); |
|||
// deciding |
|||
// done |
|||
[done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
//retry |
|||
[retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); |
|||
// loop (when finished to avoid deadlocks) |
|||
[loop] s1=3 -> 1:(s1'=3); |
|||
|
|||
endmodule |
|||
|
|||
// construct remaining processes through renaming |
|||
module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule |
|||
module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule |
|||
|
|||
// expected number of rounds |
|||
rewards "num_rounds" |
|||
[pick] true : 1; |
|||
endrewards |
|||
|
|||
// labels |
|||
label "elected" = s1=3&s2=3&s3=3; |
|||
|
|||
@ -0,0 +1,40 @@ |
|||
// sum of two dice as the asynchronous parallel composition of |
|||
// two copies of Knuth's model of a fair die using only fair coins |
|||
|
|||
mdp |
|||
|
|||
module die1 |
|||
|
|||
// local state |
|||
s1 : [0..7] init 0; |
|||
// value of the dice |
|||
d1 : [0..6] init 0; |
|||
|
|||
[] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2); |
|||
[] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4); |
|||
[] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6); |
|||
[] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1); |
|||
[] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3); |
|||
[] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5); |
|||
[] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6); |
|||
[] s1=7 & s2=7 -> 1: (s1'=7); |
|||
endmodule |
|||
|
|||
module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule |
|||
|
|||
rewards "coinflips" |
|||
[] s1<7 | s2<7 : 1; |
|||
endrewards |
|||
|
|||
label "done" = s1=7 & s2=7; |
|||
label "two" = s1=7 & s2=7 & d1+d2=2; |
|||
label "three" = s1=7 & s2=7 & d1+d2=3; |
|||
label "four" = s1=7 & s2=7 & d1+d2=4; |
|||
label "five" = s1=7 & s2=7 & d1+d2=5; |
|||
label "six" = s1=7 & s2=7 & d1+d2=6; |
|||
label "seven" = s1=7 & s2=7 & d1+d2=7; |
|||
label "eight" = s1=7 & s2=7 & d1+d2=8; |
|||
label "nine" = s1=7 & s2=7 & d1+d2=9; |
|||
label "ten" = s1=7 & s2=7 & d1+d2=10; |
|||
label "eleven" = s1=7 & s2=7 & d1+d2=11; |
|||
label "twelve" = s1=7 & s2=7 & d1+d2=12; |
|||
@ -0,0 +1,219 @@ |
|||
// WLAN PROTOCOL (two stations) |
|||
// discrete time model |
|||
// gxn/jzs 20/02/02 |
|||
|
|||
mdp |
|||
|
|||
// COLLISIONS |
|||
const int COL; // maximum number of collisions |
|||
|
|||
// TIMING CONSTRAINTS |
|||
// we have used the FHSS parameters |
|||
// then scaled by the value of ASLOTTIME |
|||
const int ASLOTTIME = 1; |
|||
const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
|||
const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
|||
const int TRANS_TIME_MAX; // scaling up |
|||
const int TRANS_TIME_MIN = 4; // scaling down |
|||
const int ACK_TO = 6; |
|||
const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
|||
const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
|||
// maximum constant used in timing constraints + 1 |
|||
const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; |
|||
|
|||
// CONTENTION WINDOW |
|||
// CWMIN =15 & CWMAX =16 |
|||
// this means that MAX_BACKOFF IS 2 |
|||
const int MAX_BACKOFF = 0; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
// THE MEDIUM/CHANNEL |
|||
|
|||
// FORMULAE FOR THE CHANNEL |
|||
// channel is busy |
|||
formula busy = c1>0 | c2>0; |
|||
// channel is free |
|||
formula free = c1=0 & c2=0; |
|||
|
|||
module medium |
|||
|
|||
// number of collisions |
|||
col : [0..COL]; |
|||
|
|||
// medium status |
|||
c1 : [0..2]; |
|||
c2 : [0..2]; |
|||
// ci corresponds to messages associated with station i |
|||
// 0 nothing being sent |
|||
// 1 being sent correctly |
|||
// 2 being sent garbled |
|||
|
|||
// begin sending message and nothing else currently being sent |
|||
[send1] c1=0 & c2=0 -> (c1'=1); |
|||
[send2] c2=0 & c1=0 -> (c2'=1); |
|||
|
|||
// begin sending message and something is already being sent |
|||
// in this case both messages become garbled |
|||
[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
|||
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
|||
|
|||
// finish sending message |
|||
[finish1] c1>0 -> (c1'=0); |
|||
[finish2] c2>0 -> (c2'=0); |
|||
|
|||
endmodule |
|||
|
|||
//-----------------------------------------------------------------// |
|||
// STATION 1 |
|||
module station1 |
|||
// clock for station 1 |
|||
x1 : [0..TIME_MAX]; |
|||
|
|||
// local state |
|||
s1 : [1..12]; |
|||
// 1 sense |
|||
// 2 wait until free before setting backoff |
|||
// 3 wait for DIFS then set slot |
|||
// 4 set backoff |
|||
// 5 backoff |
|||
// 6 wait until free in backoff |
|||
// 7 wait for DIFS then resume backoff |
|||
// 8 vulnerable |
|||
// 9 transmit |
|||
// 11 wait for SIFS and then ACK |
|||
// 10 wait for ACT_TO |
|||
// 12 done |
|||
// BACKOFF |
|||
// separate into slots |
|||
slot1 : [0..1]; |
|||
backoff1 : [0..15]; |
|||
|
|||
// BACKOFF COUNTER |
|||
bc1 : [0..1]; |
|||
// SENSE |
|||
// let time pass |
|||
[time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// ready to transmit |
|||
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0); |
|||
// found channel busy so wait until free |
|||
[] s1=1 & busy -> (s1'=2) & (x1'=0); |
|||
// WAIT UNTIL FREE BEFORE SETTING BACKOFF |
|||
// let time pass (no need for the clock x1 to change) |
|||
[time] s1=2 & busy -> (s1'=2); |
|||
// find that channel is free so check its free for DIFS before setting backoff |
|||
[] s1=2 & free -> (s1'=3); |
|||
// WAIT FOR DIFS THEN SET BACKOFF |
|||
// let time pass |
|||
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// found channel busy so wait until free |
|||
[] s1=3 & busy -> (s1'=2) & (x1'=0); |
|||
// start backoff first uniformly choose slot |
|||
// backoff counter 0 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// SET BACKOFF (no time can pass) |
|||
// chosen slot now set backoff |
|||
[] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=1 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=2 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=3 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=4 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=5 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=6 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=7 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=8 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=9 ) |
|||
+ 1/16 : (s1'=5) & (backoff1'=10) |
|||
+ 1/16 : (s1'=5) & (backoff1'=11) |
|||
+ 1/16 : (s1'=5) & (backoff1'=12) |
|||
+ 1/16 : (s1'=5) & (backoff1'=13) |
|||
+ 1/16 : (s1'=5) & (backoff1'=14) |
|||
+ 1/16 : (s1'=5) & (backoff1'=15); |
|||
// BACKOFF |
|||
// let time pass |
|||
[time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// decrement backoff |
|||
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1); |
|||
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1); |
|||
// finish backoff |
|||
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0); |
|||
// found channel busy |
|||
[] s1=5 & busy -> (s1'=6) & (x1'=0); |
|||
// WAIT UNTIL FREE IN BACKOFF |
|||
// let time pass (no need for the clock x1 to change) |
|||
[time] s1=6 & busy -> (s1'=6); |
|||
// find that channel is free |
|||
[] s1=6 & free -> (s1'=7); |
|||
|
|||
// WAIT FOR DIFS THEN RESUME BACKOFF |
|||
// let time pass |
|||
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// resume backoff (start again from previous backoff) |
|||
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0); |
|||
// found channel busy |
|||
[] s1=7 & busy -> (s1'=6) & (x1'=0); |
|||
|
|||
// VULNERABLE |
|||
// let time pass |
|||
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX)); |
|||
// move to transmit |
|||
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0); |
|||
// TRANSMIT |
|||
// let time pass |
|||
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX)); |
|||
// finish transmission successful |
|||
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0); |
|||
// finish transmission garbled |
|||
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0); |
|||
// WAIT FOR SIFS THEN WAIT FOR ACK |
|||
|
|||
// WAIT FOR SIFS i.e. c1=0 |
|||
// check channel and busy: go into backoff |
|||
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2); |
|||
// check channel and free: let time pass |
|||
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// let time pass |
|||
// following guard is always false as SIFS=1 |
|||
// [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX)); |
|||
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free) |
|||
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0); |
|||
|
|||
// WAIT FOR ACK i.e. c1=1 |
|||
// let time pass |
|||
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX)); |
|||
// get acknowledgement so packet sent correctly and move to done |
|||
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0); |
|||
|
|||
// WAIT FOR ACK_TO |
|||
// check channel and busy: go into backoff |
|||
[] s1=11 & x1=0 & busy -> (s1'=2); |
|||
// check channel and free: let time pass |
|||
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// let time pass |
|||
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX)); |
|||
// no acknowledgement (go to backoff waiting DIFS first) |
|||
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0); |
|||
|
|||
// DONE |
|||
[time] s1=12 -> (s1'=12); |
|||
|
|||
endmodule |
|||
|
|||
// ---------------------------------------------------------------------------- // |
|||
// STATION 2 (rename STATION 1) |
|||
module |
|||
station2=station1[x1=x2, |
|||
s1=s2, |
|||
s2=s1, |
|||
c1=c2, |
|||
c2=c1, |
|||
slot1=slot2, |
|||
backoff1=backoff2, |
|||
bc1=bc2, |
|||
send1=send2, |
|||
finish1=finish2] |
|||
endmodule |
|||
// ---------------------------------------------------------------------------- // |
|||
|
|||
label "twoCollisions" = col=2; |
|||
label "fourCollisions" = col=4; |
|||
label "sixCollisions" = col=6; |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue