// Danish Lakhani
// Anthony Giardullo
//
// The code below is 'annotated' PRISM code.  Using this file
// as input to preparse.java will create a valid PRISM .pm and .pctl
// file.  See the comments in preparse.java for useage information.  
//
//
//


probabilistic

//Probability a mix node is bad    
//rate badP = 0.5;
//rate goodP = 0.5; //must be 1 - bad


//const numPaths = 10;
//const maxLength = 3;
//const minLength = 3;
//const userCount = 10;
//const mixCount = 3;
//const nodeCount = 13;//must be userCount+mixCount
//const maxSearchLength = 100;
//const minSearchLength = 1;
//const useSearchLength = 1;

//rate numPathsInv = 0.1; //must be 1/numPaths

const checkSelfLoop = 0;


//Constants

*GENERATECONSTANTS*

//End Constants


//Graph

 *GENERATEGRAPH* 

//end Graph


module entropy


start:  bool init true;
launch:  bool init false;
new:  bool init false;
chooseBad:  bool init false;
done:  bool init false;
bad:  bool init false;
good: bool init false;
checkNode: bool init false;
end: bool init false;
checkEnd: bool init false;


currentNode: [0..nodeCount] init initNode;
currentPath: [0..numPaths] init 1;
success:  [0..1] init 0;
length: [0..maxSearchLength] init 0;


[] start -> (launch'=true) & (start'=false);


[] launch -> (length'=0) & (currentNode'=initNode) & (currentPath'=1) & (new'=true) & (launch'=false);


[] new & (useSearchLength != 1) -> (chooseBad'=true) & (new'=false);

[] new & (useSearchLength = 1) & (length < maxSearchLength) -> (length'=(length+1)) & (chooseBad'=true)  & (new'=false);

[] new & (useSearchLength = 1) & (length >= maxSearchLength)-> (launch'=true) & (new'=false);


[] chooseBad ->
  badP: (bad'=true) & (chooseBad'=false) +
  goodP: (good'=true) & (chooseBad'=false);


{n 1 nodeCount p 1 numPaths}[] bad & (currentNode = {n}) & (currentPath = {p})  -> (currentNode'=node{n}path{p}) & (bad'=false) & (end'=true);



2{n 1 nodeCount}[] good & (currentNode = {n}) ->
{p 1 numPaths} numPathsInv: (currentNode'=(node{n}path{p} * min(1,node{n}path{p}) - currentNode*(min(1, node{n}path{p}) - 1))) &  (currentPath'=({p} * min(1, node{n}path{p}) - currentPath*(min(1,node{n}path{p}) - 1))) & (success'=min(1, node{n}path{p})) & (checkNode'=true) & (good'=false)+



[]checkNode & !success -> (good'=true) & (checkNode'=false);

[]checkNode & success -> (success'=false) & (end'=true) & (checkNode'=false);


[]end & (currentNode <= userCount) & (useSearchLength != 1) -> (checkEnd'=true) & (end'=false);

[]end & (currentNode <= userCount) & (useSearchLength = 1) & (length >= minSearchLength) -> (checkEnd'=true) & (end'=false);

[]end & (currentNode <= userCount) & (useSearchLength = 1) & (length < minSearchLength) -> (launch'=true) & (end'=false);

[]end & (currentNode > userCount) -> (new'=true) & (end'=false);


[]checkEnd & ((currentNode != initNode) | (checkSelfLoop = 0)) -> (done'=true) & (checkEnd'=false);

[]checkEnd & (currentNode = initNode) & (checkSelfLoop = 1) -> (launch'=true) & (checkEnd'=false);


[]done -> (done'=true);



endmodule