Commit 07056b96 authored by Lars Schieffer's avatar Lars Schieffer
Browse files

update tests

parent 8327633e
#QCOMP
##DTMC
wget http://qcomp.org/benchmarks/dtmc/brp/brp.jani -O dtmc/brp/brp.jani
wget http://qcomp.org/benchmarks/dtmc/coupon/coupon.5-2.jani -O dtmc/coupon/coupon.5-2.jani
wget http://qcomp.org/benchmarks/dtmc/leader_sync/leader_sync.3-2.jani -O dtmc/leader_sync/leader_sync.3-2.jani
wget http://qcomp.org/benchmarks/dtmc/egl/egl.jani -O dtmc/egl/egl.v1.jani
##MDP
wget http://qcomp.org/benchmarks/mdp/beb/beb.3-4.jani -O mdp/beb/beb.3-4.jani
wget http://qcomp.org/benchmarks/mdp/consensus/consensus.2.jani -O mdp/consensus/consensus.2.v1.jani
wget http://qcomp.org/benchmarks/mdp/csma/csma.2-2.jani -O mdp/csma/csma.2-2.v1.jani
wget http://qcomp.org/benchmarks/mdp/elevators/elevators.a-3-3.jani -O mdp/elevators/elevators.a-3-3.v1.jani
wget http://qcomp.org/benchmarks/mdp/rectangle-tireworld/rectangle-tireworld.5.jani -O mdp/rectangle-tireworld/rectangle-tireworld.5.v1.jani
wget http://qcomp.org/benchmarks/mdp/tireworld/tireworld.17.jani -O mdp/tireworld/tireworld.17.v1.jani
wget http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani -O mdp/wlan/wlan.0.v1.jani
\ No newline at end of file
wget -i modelSources/qcomp.txt -P ./jani/qcomp -N
This diff is collapsed.
#include <jani2pinsPlugin.h>
#ifndef GROUPAMOUNT
#define GROUPAMOUNT 801
#endif
//Create TransitionGroupGuards
guard_t **createTransitionGroupGuardInformation()
{
// Guards of each transition group
int *transitionGuards[GROUPAMOUNT] = {(int[]){0,1},(int[]){1,2},(int[]){1,3},(int[]){1,4},(int[]){0,1},(int[]){1,2},(int[]){1,3},(int[]){1,4},(int[]){0,5},(int[]){2,5},(int[]){3,5},(int[]){4,5},(int[]){0,5},(int[]){2,5},(int[]){3,5},(int[]){4,5},(int[]){0,6},(int[]){2,6},(int[]){3,6},(int[]){4,6},(int[]){0,6},(int[]){2,6},(int[]){3,6},(int[]){4,6},(int[]){0,7},(int[]){2,7},(int[]){3,7},(int[]){4,7},(int[]){0,7},(int[]){2,7},(int[]){3,7},(int[]){4,7},(int[]){0,8},(int[]){2,8},(int[]){3,8},(int[]){4,8},(int[]){0,8},(int[]){2,8},(int[]){3,8},(int[]){4,8},(int[]){0,9},(int[]){2,9},(int[]){3,9},(int[]){4,9},(int[]){0,9},(int[]){2,9},(int[]){3,9},(int[]){4,9},(int[]){0,10},(int[]){10,2},(int[]){10,3},(int[]){10,4},(int[]){0,10},(int[]){10,2},(int[]){10,3},(int[]){10,4},(int[]){0,11},(int[]){11,2},(int[]){11,3},(int[]){11,4},(int[]){0,11},(int[]){11,2},(int[]){11,3},(int[]){11,4},(int[]){0,12},(int[]){12,2},(int[]){12,3},(int[]){12,4},(int[]){0,12},(int[]){12,2},(int[]){12,3},(int[]){12,4},(int[]){0,13},(int[]){13,2},(int[]){13,3},(int[]){13,4},(int[]){0,13},(int[]){13,2},(int[]){13,3},(int[]){13,4},(int[]){0,14},(int[]){14,2},(int[]){14,3},(int[]){14,4},(int[]){0,14},(int[]){14,2},(int[]){14,3},(int[]){14,4},(int[]){0,15},(int[]){15,2},(int[]){15,3},(int[]){15,4},(int[]){0,15},(int[]){15,2},(int[]){15,3},(int[]){15,4},(int[]){0,16},(int[]){16,2},(int[]){16,3},(int[]){16,4},(int[]){0,16},(int[]){16,2},(int[]){16,3},(int[]){16,4},(int[]){0,17},(int[]){17,2},(int[]){17,3},(int[]){17,4},(int[]){0,17},(int[]){17,2},(int[]){17,3},(int[]){17,4},(int[]){0,18},(int[]){18,2},(int[]){18,3},(int[]){18,4},(int[]){0,18},(int[]){18,2},(int[]){18,3},(int[]){18,4},(int[]){0,19},(int[]){19,2},(int[]){19,3},(int[]){19,4},(int[]){0,19},(int[]){19,2},(int[]){19,3},(int[]){19,4},(int[]){0,20},(int[]){2,20},(int[]){20,3},(int[]){20,4},(int[]){0,20},(int[]){2,20},(int[]){20,3},(int[]){20,4},(int[]){0,21},(int[]){2,21},(int[]){21,3},(int[]){21,4},(int[]){0,21},(int[]){2,21},(int[]){21,3},(int[]){21,4},(int[]){0,22},(int[]){2,22},(int[]){22,3},(int[]){22,4},(int[]){0,22},(int[]){2,22},(int[]){22,3},(int[]){22,4},(int[]){0,23},(int[]){2,23},(int[]){23,3},(int[]){23,4},(int[]){0,23},(int[]){2,23},(int[]){23,3},(int[]){23,4},(int[]){0,24},(int[]){2,24},(int[]){24,3},(int[]){24,4},(int[]){0,25},(int[]){2,25},(int[]){25,3},(int[]){25,4},(int[]){0,26},(int[]){2,26},(int[]){26,3},(int[]){26,4},(int[]){0,27},(int[]){2,27},(int[]){27,3},(int[]){27,4},(int[]){0,28},(int[]){2,28},(int[]){28,3},(int[]){28,4},(int[]){0,29},(int[]){2,29},(int[]){29,3},(int[]){29,4},(int[]){0,30},(int[]){2,30},(int[]){3,30},(int[]){30,4},(int[]){0,31},(int[]){2,31},(int[]){3,31},(int[]){31,4},(int[]){0,32},(int[]){2,32},(int[]){3,32},(int[]){32,4},(int[]){0,33},(int[]){2,33},(int[]){3,33},(int[]){33,4},(int[]){0,34},(int[]){2,34},(int[]){3,34},(int[]){34,4},(int[]){0,35},(int[]){2,35},(int[]){3,35},(int[]){35,4},(int[]){0,36},(int[]){2,36},(int[]){3,36},(int[]){36,4},(int[]){0,37},(int[]){2,37},(int[]){3,37},(int[]){37,4},(int[]){0,38},(int[]){2,38},(int[]){3,38},(int[]){38,4},(int[]){0,39},(int[]){2,39},(int[]){3,39},(int[]){39,4},(int[]){0,40},(int[]){2,40},(int[]){3,40},(int[]){4,40},(int[]){0,41},(int[]){2,41},(int[]){3,41},(int[]){4,41},(int[]){0,42},(int[]){2,42},(int[]){3,42},(int[]){4,42},(int[]){0,43},(int[]){2,43},(int[]){3,43},(int[]){4,43},(int[]){0,44},(int[]){2,44},(int[]){3,44},(int[]){4,44},(int[]){0,45},(int[]){2,45},(int[]){3,45},(int[]){4,45},(int[]){0,46},(int[]){2,46},(int[]){3,46},(int[]){4,46},(int[]){0,47},(int[]){2,47},(int[]){3,47},(int[]){4,47},(int[]){0,48},(int[]){2,48},(int[]){3,48},(int[]){4,48},(int[]){0,49},(int[]){2,49},(int[]){3,49},(int[]){4,49},(int[]){0,50},(int[]){2,50},(int[]){3,50},(int[]){4,50},(int[]){0,51},(int[]){2,51},(int[]){3,51},(int[]){4,51},(int[]){0,52},(int[]){2,52},(int[]){3,52},(int[]){4,52},(int[]){0,53},(int[]){2,53},(int[]){3,53},(int[]){4,53},(int[]){0,54},(int[]){2,54},(int[]){3,54},(int[]){4,54},(int[]){0,55},(int[]){2,55},(int[]){3,55},(int[]){4,55},(int[]){0,56},(int[]){2,56},(int[]){3,56},(int[]){4,56},(int[]){0,57},(int[]){2,57},(int[]){3,57},(int[]){4,57},(int[]){0,58},(int[]){2,58},(int[]){3,58},(int[]){4,58},(int[]){0,59},(int[]){2,59},(int[]){3,59},(int[]){4,59},(int[]){0,60},(int[]){2,60},(int[]){3,60},(int[]){4,60},(int[]){0,61},(int[]){2,61},(int[]){3,61},(int[]){4,61},(int[]){0,62},(int[]){2,62},(int[]){3,62},(int[]){4,62},(int[]){0,63},(int[]){2,63},(int[]){3,63},(int[]){4,63},(int[]){64,65},(int[]){65,66},(int[]){65,67},(int[]){65,68},(int[]){65,69},(int[]){65,70},(int[]){64,65},(int[]){65,66},(int[]){65,67},(int[]){65,68},(int[]){65,69},(int[]){65,70},(int[]){64,71},(int[]){66,71},(int[]){67,71},(int[]){68,71},(int[]){69,71},(int[]){70,71},(int[]){64,71},(int[]){66,71},(int[]){67,71},(int[]){68,71},(int[]){69,71},(int[]){70,71},(int[]){64,72},(int[]){66,72},(int[]){67,72},(int[]){68,72},(int[]){69,72},(int[]){70,72},(int[]){64,72},(int[]){66,72},(int[]){67,72},(int[]){68,72},(int[]){69,72},(int[]){70,72},(int[]){64,73},(int[]){66,73},(int[]){67,73},(int[]){68,73},(int[]){69,73},(int[]){70,73},(int[]){64,73},(int[]){66,73},(int[]){67,73},(int[]){68,73},(int[]){69,73},(int[]){70,73},(int[]){64,74},(int[]){66,74},(int[]){67,74},(int[]){68,74},(int[]){69,74},(int[]){70,74},(int[]){64,74},(int[]){66,74},(int[]){67,74},(int[]){68,74},(int[]){69,74},(int[]){70,74},(int[]){64,75},(int[]){66,75},(int[]){67,75},(int[]){68,75},(int[]){69,75},(int[]){70,75},(int[]){64,75},(int[]){66,75},(int[]){67,75},(int[]){68,75},(int[]){69,75},(int[]){70,75},(int[]){64,76},(int[]){66,76},(int[]){67,76},(int[]){68,76},(int[]){69,76},(int[]){70,76},(int[]){64,76},(int[]){66,76},(int[]){67,76},(int[]){68,76},(int[]){69,76},(int[]){70,76},(int[]){64,77},(int[]){66,77},(int[]){67,77},(int[]){68,77},(int[]){69,77},(int[]){70,77},(int[]){64,77},(int[]){66,77},(int[]){67,77},(int[]){68,77},(int[]){69,77},(int[]){70,77},(int[]){64,78},(int[]){66,78},(int[]){67,78},(int[]){68,78},(int[]){69,78},(int[]){70,78},(int[]){64,78},(int[]){66,78},(int[]){67,78},(int[]){68,78},(int[]){69,78},(int[]){70,78},(int[]){64,79},(int[]){66,79},(int[]){67,79},(int[]){68,79},(int[]){69,79},(int[]){70,79},(int[]){64,79},(int[]){66,79},(int[]){67,79},(int[]){68,79},(int[]){69,79},(int[]){70,79},(int[]){64,80},(int[]){66,80},(int[]){67,80},(int[]){68,80},(int[]){69,80},(int[]){70,80},(int[]){64,80},(int[]){66,80},(int[]){67,80},(int[]){68,80},(int[]){69,80},(int[]){70,80},(int[]){64,81},(int[]){66,81},(int[]){67,81},(int[]){68,81},(int[]){69,81},(int[]){70,81},(int[]){64,81},(int[]){66,81},(int[]){67,81},(int[]){68,81},(int[]){69,81},(int[]){70,81},(int[]){64,82},(int[]){66,82},(int[]){67,82},(int[]){68,82},(int[]){69,82},(int[]){70,82},(int[]){64,82},(int[]){66,82},(int[]){67,82},(int[]){68,82},(int[]){69,82},(int[]){70,82},(int[]){64,83},(int[]){66,83},(int[]){67,83},(int[]){68,83},(int[]){69,83},(int[]){70,83},(int[]){64,83},(int[]){66,83},(int[]){67,83},(int[]){68,83},(int[]){69,83},(int[]){70,83},(int[]){64,84},(int[]){66,84},(int[]){67,84},(int[]){68,84},(int[]){69,84},(int[]){70,84},(int[]){64,84},(int[]){66,84},(int[]){67,84},(int[]){68,84},(int[]){69,84},(int[]){70,84},(int[]){64,85},(int[]){66,85},(int[]){67,85},(int[]){68,85},(int[]){69,85},(int[]){70,85},(int[]){64,85},(int[]){66,85},(int[]){67,85},(int[]){68,85},(int[]){69,85},(int[]){70,85},(int[]){64,86},(int[]){66,86},(int[]){67,86},(int[]){68,86},(int[]){69,86},(int[]){70,86},(int[]){64,86},(int[]){66,86},(int[]){67,86},(int[]){68,86},(int[]){69,86},(int[]){70,86},(int[]){64,87},(int[]){66,87},(int[]){67,87},(int[]){68,87},(int[]){69,87},(int[]){70,87},(int[]){64,87},(int[]){66,87},(int[]){67,87},(int[]){68,87},(int[]){69,87},(int[]){70,87},(int[]){64,88},(int[]){66,88},(int[]){67,88},(int[]){68,88},(int[]){69,88},(int[]){70,88},(int[]){64,88},(int[]){66,88},(int[]){67,88},(int[]){68,88},(int[]){69,88},(int[]){70,88},(int[]){64,89},(int[]){66,89},(int[]){67,89},(int[]){68,89},(int[]){69,89},(int[]){70,89},(int[]){64,89},(int[]){66,89},(int[]){67,89},(int[]){68,89},(int[]){69,89},(int[]){70,89},(int[]){64,90},(int[]){66,90},(int[]){67,90},(int[]){68,90},(int[]){69,90},(int[]){70,90},(int[]){64,91},(int[]){66,91},(int[]){67,91},(int[]){68,91},(int[]){69,91},(int[]){70,91},(int[]){64,92},(int[]){66,92},(int[]){67,92},(int[]){68,92},(int[]){69,92},(int[]){70,92},(int[]){64,93},(int[]){66,93},(int[]){67,93},(int[]){68,93},(int[]){69,93},(int[]){70,93},(int[]){64,94},(int[]){66,94},(int[]){67,94},(int[]){68,94},(int[]){69,94},(int[]){70,94},(int[]){64,95},(int[]){66,95},(int[]){67,95},(int[]){68,95},(int[]){69,95},(int[]){70,95},(int[]){64,96},(int[]){66,96},(int[]){67,96},(int[]){68,96},(int[]){69,96},(int[]){70,96},(int[]){64,97},(int[]){66,97},(int[]){67,97},(int[]){68,97},(int[]){69,97},(int[]){70,97},(int[]){64,98},(int[]){66,98},(int[]){67,98},(int[]){68,98},(int[]){69,98},(int[]){70,98},(int[]){64,99},(int[]){66,99},(int[]){67,99},(int[]){68,99},(int[]){69,99},(int[]){70,99},(int[]){100,64},(int[]){100,66},(int[]){100,67},(int[]){100,68},(int[]){100,69},(int[]){100,70},(int[]){101,64},(int[]){101,66},(int[]){101,67},(int[]){101,68},(int[]){101,69},(int[]){101,70},(int[]){102,64},(int[]){102,66},(int[]){102,67},(int[]){102,68},(int[]){102,69},(int[]){102,70},(int[]){103,64},(int[]){103,66},(int[]){103,67},(int[]){103,68},(int[]){103,69},(int[]){103,70},(int[]){104,64},(int[]){104,66},(int[]){104,67},(int[]){104,68},(int[]){104,69},(int[]){104,70},(int[]){105,64},(int[]){105,66},(int[]){105,67},(int[]){105,68},(int[]){105,69},(int[]){105,70},(int[]){106,64},(int[]){106,66},(int[]){106,67},(int[]){106,68},(int[]){106,69},(int[]){106,70},(int[]){107,64},(int[]){107,66},(int[]){107,67},(int[]){107,68},(int[]){107,69},(int[]){107,70},(int[]){108,64},(int[]){108,66},(int[]){108,67},(int[]){108,68},(int[]){108,69},(int[]){108,70},(int[]){109,64},(int[]){109,66},(int[]){109,67},(int[]){109,68},(int[]){109,69},(int[]){109,70},(int[]){110,64},(int[]){110,66},(int[]){110,67},(int[]){110,68},(int[]){110,69},(int[]){110,70},(int[]){111,64},(int[]){111,66},(int[]){111,67},(int[]){111,68},(int[]){111,69},(int[]){111,70},(int[]){112,64},(int[]){112,66},(int[]){112,67},(int[]){112,68},(int[]){112,69},(int[]){112,70},(int[]){113,64},(int[]){113,66},(int[]){113,67},(int[]){113,68},(int[]){113,69},(int[]){113,70},(int[]){114,64},(int[]){114,66},(int[]){114,67},(int[]){114,68},(int[]){114,69},(int[]){114,70},(int[]){115,64},(int[]){115,66},(int[]){115,67},(int[]){115,68},(int[]){115,69},(int[]){115,70},(int[]){116,64},(int[]){116,66},(int[]){116,67},(int[]){116,68},(int[]){116,69},(int[]){116,70},(int[]){117,64},(int[]){117,66},(int[]){117,67},(int[]){117,68},(int[]){117,69},(int[]){117,70},(int[]){118,64},(int[]){118,66},(int[]){118,67},(int[]){118,68},(int[]){118,69},(int[]){118,70},(int[]){119,64},(int[]){119,66},(int[]){119,67},(int[]){119,68},(int[]){119,69},(int[]){119,70},(int[]){120,64},(int[]){120,66},(int[]){120,67},(int[]){120,68},(int[]){120,69},(int[]){120,70},(int[]){121,64},(int[]){121,66},(int[]){121,67},(int[]){121,68},(int[]){121,69},(int[]){121,70},(int[]){122,64},(int[]){122,66},(int[]){122,67},(int[]){122,68},(int[]){122,69},(int[]){122,70},(int[]){123,64},(int[]){123,66},(int[]){123,67},(int[]){123,68},(int[]){123,69},(int[]){123,70},(int[]){124,64},(int[]){124,66},(int[]){124,67},(int[]){124,68},(int[]){124,69},(int[]){124,70},(int[]){125,64},(int[]){125,66},(int[]){125,67},(int[]){125,68},(int[]){125,69},(int[]){125,70},(int[]){126,64},(int[]){126,66},(int[]){126,67},(int[]){126,68},(int[]){126,69},(int[]){126,70},(int[]){127,64},(int[]){127,66},(int[]){127,67},(int[]){127,68},(int[]){127,69},(int[]){127,70},(int[]){128,64},(int[]){128,66},(int[]){128,67},(int[]){128,68},(int[]){128,69},(int[]){128,70},(int[]){129,64},(int[]){129,66},(int[]){129,67},(int[]){129,68},(int[]){129,69},(int[]){129,70},(int[]){130}};
int transitionGuardsSizes[GROUPAMOUNT] = {2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,2,1};
guard_t **guard_info = malloc(GROUPAMOUNT * sizeof(guard_t *));
for (int i = 0; i < GROUPAMOUNT; i++)
{
guard_info[i] = malloc(sizeof(int[transitionGuardsSizes[i] + 1]));
memcpy(guard_info[i]->guard, transitionGuards[i], transitionGuardsSizes[i] * sizeof(int));
guard_info[i]->count = transitionGuardsSizes[i];
}
return guard_info;
}
#include <jani2pinsPlugin.h>
// Name of the PINS plugin
char pins_plugin_name[] = "jani2pins";
// Compute the remainder of Euclidean division
int remEuc(int x, int y){
int remainder = x % y;
if (remainder < 0){
return remainder + abs(y);
}
else{
return remainder;
}
}
// Compute the signum function
int sgn(int x){
if (x>0){
return 1;
}
if (x<0){
return -1;
}
return 0;
}
// Evaluate all state labels or guard
static void stateLabelsGroup(model_t model, sl_group_enum_t group, int *sourceStateVector, int *stateVectorLabels) {
if (group == GB_SL_GUARDS) {
for (int i = 0; i < guardAmount(); i++) {
stateVectorLabels[i] = stateVectorLabelLong(model, i, sourceStateVector);
}
}
if (group == GB_SL_ALL) {
for (int i = 0; i < labelAmount(); i++) {
stateVectorLabels[i] = stateVectorLabelLong(model, i, sourceStateVector);
}
}
}
// Initialise LTSmin Model
void pins_model_init(model_t model) {
// Initialise pins model
initModel(model);
// Set initial state
GBsetInitialState(model, initialStateVector());
//Set pointer to next-state function
GBsetNextStateLong(model, (next_method_grey_t)nextStateLong);
GBsetNextStateShortR2W(model, (next_method_grey_t)nextStateR2W);
GBsetActionsShortR2W(model, (next_method_grey_t)actionsR2W);
//Set pointer to label evaluation function
GBsetStateLabelLong(model, (get_label_method_t)stateVectorLabelLong);
GBsetStateLabelShort(model, (get_label_method_t)stateVectorLabelShort);
// Add new implementation
GBsetStateLabelsGroup(model, stateLabelsGroup);
// Create dependent matrices
matrix_t *rm = malloc(sizeof(matrix_t));
matrix_t *wm = malloc(sizeof(matrix_t));
matrix_t *cm = malloc(sizeof(matrix_t));
matrix_t *lm = malloc(sizeof(matrix_t));
matrix_t *dna = malloc(sizeof(matrix_t));
matrix_t *nes = malloc(sizeof(matrix_t));
matrix_t *nds = malloc(sizeof(matrix_t));
matrix_t *mce = malloc(sizeof(matrix_t));
dm_create(rm, groupAmount(), stateVectorLength());
dm_create(wm, groupAmount(), stateVectorLength());
dm_create(cm, groupAmount(), stateVectorLength());
dm_create(lm, labelAmount(), stateVectorLength());
dm_create(dna, groupAmount(), groupAmount());
dm_create(nes, guardAmount(), groupAmount());
dm_create(nds, guardAmount(), groupAmount());
dm_create(mce, guardAmount(), guardAmount());
// Set read & write dependency matrices
for (int i = 0; i < groupAmount(); i++) {
for (int j = 0; j < stateVectorLength(); j++) {
if (readDependencies(i)[j]) {
dm_set(cm, i, j);
dm_set(rm, i, j);
}
if (writeDependencies(i)[j]) {
dm_set(cm, i, j);
dm_set(wm, i, j);
}
}
}
// Set label dependency matrix
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < stateVectorLength(); j++) {
if (labelDependencies(i)[j]) {
dm_set(lm, i, j);
}
}
}
// Set do-not-accord matrix
for (int i = 0; i < groupAmount(); i++) {
for (int j = 0; j < groupAmount(); j++) {
if (dnaGroup(i)[j]) {
dm_set(dna, i, j);
}
}
}
// Set necessary enabling set and necessary disabling set
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < groupAmount(); j++) {
if (necessaryEnabling(i)[j]) {
dm_set(nes, i, j);
}
if (necessaryDisabling(i)[j]) {
dm_set(nds, i, j);
}
}
}
// Set may-be-co-enabled matrix
for (int i = 0; i < labelAmount(); i++) {
for (int j = 0; j < labelAmount(); j++) {
if (maybeCoEnabled(i)[j]) {
dm_set(mce, i, j);
}
}
}
// Set pointer to dependency matrices
GBsetDMInfoRead(model, rm);
GBsetDMInfoMustWrite(model, wm);
GBsetDMInfo(model, cm);
GBsetStateLabelInfo(model, lm);
GBsetDoNotAccordInfo(model, dna);
GBsetGuardNESInfo(model, nes);
GBsetGuardNDSInfo(model, nds);
GBsetGuardCoEnabledInfo(model, mce);
// Create Label Mapping
sl_group_t *sl_group_all = malloc(labelAmount() * sizeof(sl_group_all));
sl_group_all->count = labelAmount();
for (int i = 0; i < labelAmount(); i++) {
sl_group_all->sl_idx[i] = i;
}
// Create Guard Mapping
sl_group_t *sl_group_guards = malloc(guardAmount() * sizeof(sl_group_guards));
sl_group_guards->count = guardAmount();
for (int i = 0; i < guardAmount(); i++) {
sl_group_guards->sl_idx[i] = i;
}
// Set pointer to label & guard mappings
GBsetStateLabelGroupInfo(model, GB_SL_ALL, sl_group_all);
GBsetStateLabelGroupInfo(model, GB_SL_GUARDS, sl_group_guards);
// Add Action guards
GBsetGuardsInfo(model, createTransitionGroupGuardInformation());
// Printing Guards in stdout
GBprintStateLabelGroupInfo(stdout, model);
}
\ No newline at end of file
#include <ltsmin/dlopen-api.h>
#include <ltsmin/lts-type.h>
#include <ltsmin/ltsmin-standard.h>
#include <ltsmin/pins-util.h>
#include <ltsmin/pins.h>
#include <math.h>
//
// model.c
//
// The amount of all defined groups
int groupAmount();
// The amount of all defined labels
int labelAmount();
// The amount of all defined guards
int guardAmount();
// The length of the whole state vector
int stateVectorLength();
// Initialise the PINS model
void initModel(model_t model);
// Implementation of calculating remainder of Euclidean division
int remEuc(int x, int y);
// Compute the signum function
int sgn(int x);
//
// next-states.c
//
// The initial state vector
int *initialStateVector();
// Successor function for PINS model using a LONG state vector.
int nextStateLong(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Successor function for PINS model using a R2W state vector.
int nextStateR2W(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Update function for PINS model using a R2W state vector.
int actionsR2W(model_t model, int group, int *state_src, TransitionCB callback, void *context);
// Label function for LONG state vector:
int stateVectorLabelLong(model_t model, int label, int *state_src);
// Label function for SHORT state vector:
int stateVectorLabelShort(model_t model, int label, int *state_src);
//
// dependencies.c
//
// Read dependencies to state vector
int *readDependencies(int group);
// Write Dependencies
int *writeDependencies(int group);
// Label Dependencies
int *labelDependencies(int label);
// Do not accord
int *dnaGroup(int group);
// Necessary Enabling
int *necessaryEnabling(int guard);
// Necessary Disabling
int *necessaryDisabling(int guard);
// Maybe co-enabled
int *maybeCoEnabled(int guard);
//
// guards.c
//
//Create Action Guards
guard_t **createTransitionGroupGuardInformation();
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
# Models were taken from qcomp quantitative verification 2020 benchmark set.
# http://qcomp.org/ [last accessed 23.04.2020]
http://qcomp.org/benchmarks/mdp/beb/beb.3-4.jani
http://qcomp.org/benchmarks/mdp/consensus/consensus.2.jani
http://qcomp.org/benchmarks/mdp/csma/csma.2-2.jani
http://qcomp.org/benchmarks/mdp/elevators/elevators.a-3-3.jani
http://qcomp.org/benchmarks/mdp/exploding-blocksworld/exploding-blocksworld.5.jani
http://qcomp.org/benchmarks/mdp/pnueli-zuck/pnueli-zuck.3.jani
http://qcomp.org/benchmarks/mdp/rabin/rabin.3.jani
http://qcomp.org/benchmarks/mdp/triangle-tireworld/triangle-tireworld.9.jani
http://qcomp.org/benchmarks/mdp/wlan/wlan.0.jani
......@@ -11,6 +11,7 @@ transformations = [
("tests/res/lts/nonNDND/nonNDND.jani", ""),
("tests/res/dtmc/brp/brp.jani", "N=16,MAX=3"),
("tests/res/dtmc/coupon/coupon.5-2.jani", "B=5"),
("tests/res/dtmc/egl/egl.v1.jani", "N=5, L=2"),
("tests/res/dtmc/leader_sync/leader_sync.3-2.jani", ""),
("tests/res/mdp/beb/beb.3-4.jani", "N=3"),
("tests/res/mdp/consensus/consensus.2.v1.jani", "K=2"),
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment