Probabilistic model checker
Clone the repo
git clone https://github.com/pranshugaba/partial-exploration.git
Clone all the submodules
git submodule update --init --checkout --recursive
Build necessary submodules
cd lib/models/lib/prism/prism # navigate to folder
make # build
Build partial-explorer
cd ../../../../.. # navigate to folder
./gradlew compileJava # build
To run, reachability checker
./gradlew -p ./ run --args='reachability -m data/models/zeroconf.prism -p data/models/zeroconf.props --property correct_max --const N=1000,K=8,reset=false'
To run, mean-payoff checker
./gradlew -p ./ run --args='meanPayoff -m data/models/zeroconf_rewards.prism --precision 0.01 --maxReward 1 --revisitThreshold 2 -c N=40,K=10,reset=false --rewardModule avoid'
- Select Add Configuration(Present at top right in intellij) option. Select configuration type to be Application and specify the following parameters
- Set module as Java 11 or above
- Classpath: partial-exploration.main
- Main class: de.tum.in.pet.Main
- To enable assertions, make sure Add VM options flag is enabled in Modify options. Then add "-ea" string in VM options.
- Command line arguments:
meanPayoff -m data/models/zeroconf_rewards.prism --precision 0.01 --maxReward 1 --revisitThreshold 2 -c N=40,K=10,reset=false --rewardModule avoid