DotAndBoxes

Hello,

I kind of promised a comment about the DotAndBoxes models. The discussion here is difficult since there are no equivalent unfolded P/T models available.

Also, the behavior of the colored model is quite different from the actual game. Positions are taken from a circular enumeration (so we could infer that the game is played on a torus) but this does not seem to be the case. Also, some moves are not possible on the model compared with the game. For instance, for Dot2, the game is stuck if Player1 start playing at a position different from (0,0) because neither transitions Lose1 or Win1 can fire. The same occurs with Dot3 if Player1 starts playing at position (x, y) with x > 1 or y > 1.

ITS and Marcie both agree on the number of reachable states. 11 for Dot2 and 383 for Dot3.

I find only 27 reachable states for Dot3. I also find that transition Lose2 never fires; actually Player2  never play. Could one of the organiser please exhibit a trace where Player2 can make a move on model Dot3 ?


Silvano

In fact, there was a long discussion about this model. As far as I remember, the unfolding of this one is particularly non-trivial and our unfolders had troubles to process it for a reason I do not remember right now (it was 4 years ago). So this is an exception and it is normal that you do not fins a P/T equivalent for this model... nobody is perfect ;-)

My comment said that I did find an unfolding of the High-level net. (Maybe there is a condition or an operator that I missed in my translation but I think that all the traps where covered in other models, like double subtraction or occurrences of All in edges).

My problem is that I do not find the same number of states that other tools and I think that the state graph that I generate is correct with respect to the PNML file. I must admit that this model is quite complicated and that it is difficult to understand all its detail in a day! What I find with my tool is consistent with my "manual" exploration of the state space. This is why I ask for someone to please exhibit "a trace where Player2 can make a move on model Dot3". If it exists it should be quite short, at most 3 or 4 transitions long.

Also, given the problem that I found with PhiloDyn, I am not sure that I have been working with the same PNML files that those used during the previous contest. I have downloaded the XML files directly from mcc.lip6.fr/archives.

Once again, the model is very complicated and I am far less sure that there is a problem with DotandBoxes than, say, PhiloDyn.

Two answers:

1) we can discuss with the author of DotAndBoxes to check for the correctness of the unfolding of a small instance (at least). If we come to a satisfactory situation, then we can propose the P/T equivalent model

2) Of course, the PNML files will never be updated without notice during the contest. Either any bug will be fixed this year and all tools developers will be notified, or the correction will appear for next year.

Do not be worried, we already had bug detected by tools developers in the past and they have been corrected, the same year or the year after according to when they where detected (and our capability to handle corrections on time while keeping good conditions for the contest.

Hi

Just a few remarks :
a) Both Marcie and ITS-tools are available publicly, you can test yourself/ask for a trace leading to certain states etc... Give that your graph is so small, manual inspection should allow to debug. Please ask if you need help running ITS-tools, I can give you a short instructions to get a model from the CPN that you can inspect for differences with you own model.

b) Don't fight the majority, if we agree (Christian's Marcie and ITS tools), we are probably right. In any case, if you answer something different than us, you'll get negative points and bad confidence scores. Remember that the "correct" answer is determined using a consensus.

Thanks for the proposal to help.

I have contacted the author of the model to help me find what (or if) I understand incorrectly.

I have not yet installed the other tools. Running them is easy, but finding the right syntax for the reachability formulas and/or interpreting the results takes more time ;-)

This is why I asked in my initial question whether one of the tool was able to exhibit a run leading to a state where Player2 can play in the Dot3 model. For a start, a state where Lose2 can fire will be OK.

Once I see how your tool can find such a trace (e.g. the syntax of the formula), I may try to dig deeper.

Again, thanks for your support.

Hi,

Below is the result of my own transformation, I asked for a trace to End[1]=1, which I think is what you want.
property player2plays [reachable] : End[1]==1;


[ Score[10]=1 FreePositions[17]=1 FreePositions[16]=1 FreePositions[15]=1 FreePositions[14]=1 FreePositions[7]=1 FreePositions[13]=1 FreePositions[6]=1 FreePositions[12]=1 FreePositions[4]=1 Idle[0]=1 FreePositions[3]=1 FreePositions[1]=1 FreePositions[11]=1 FreePositions[10]=1 FreePositions[0]=1 FreePositions[9]=1 FreePositions[8]=1 FreePositions[5]=1 FreePositions[2]=1 IsWinner[3]=1 IsWinner[1]=1 Score[0]=1 ]

This shortest transition sequence of length 7 :
Play_0_0_0_1, Lose1_0_0_0_0_0_2_1, Lose2_0_0_0_0_0_0_1, NoWin_0, Play_1_0_1_1, Lose1_1_0_1_1_0_2_1, Lose2_1_0_1_1_0_0_1
Leads to final states :
[ Score[10]=1 FreePositions[17]=1 FreePositions[16]=1 FreePositions[15]=1 FreePositions[14]=1 FreePositions[7]=1 FreePositions[13]=1 FreePositions[6]=1 OccupiedPositions[4]=1 FreePositions[12]=1 End[1]=1 OccupiedPositions[3]=1 FreePositions[1]=1 FreePositions[11]=1 FreePositions[10]=1 FreePositions[0]=1 FreePositions[9]=1 FreePositions[8]=1 FreePositions[5]=1 FreePositions[2]=1 IsWinner[3]=1 IsWinner[1]=1 Score[0]=1 ]


In any case you can add other queries if you need pretty easily.
To try it:
* install eclipse neon (any version)
* install->New Software -> add update site : https: / / lip6.github.io/ITSTools/
* select "all in one", and/or pnmcc feature from incubation

Add the attached file to a project, make sure extension is .gal
Edit the properties (bottom of file) with the nice editor.
You can also right-click pnml files and select "PNML to GAL -> transform to GAL".
(if you don't see the files, make sure you hit File->Refresh on the containing folder as new files are not always visible in eclipse (platform dependent).)

Right-click a gal file -> run As -> ITS model-check to get witness traces etc...

In any case, the target of my transformation is quite easy to read (size ~ colored petri net size), hope it helps you debug.
We lack multidimensional arrays so there is some arithmetic to get the right array index when considering places with cross product domain, the multipliers that occur in the code are sizes of the lesser array dimensions.

Code:



gal DotAndBoxes_COL_3{
  typedef Player= 0..1 ;
  typedef Direction= 0..1 ;
  typedef Position= 0..2 ;
  typedef Count= 0..9 ;
  typedef Bool= 0..1 ;
  /** Place Idle dom :Player*/
  array [2]Idle = (1, 0 );
  /** Place Score dom :PlayerCount*/
  array [20]Score = (1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
  /** Place FreePositions dom :Positions*/
  array [18]FreePositions = (1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 );
  /** Place OccupiedPositions dom :Positions*/
  array [18]OccupiedPositions = (0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
  /** Place Chosed dom :Played*/
  array [36]Chosed = (0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
  /** Place IsWinner dom :PlayerBool*/
  array [4]IsWinner = (0, 1, 0, 1 );
  /** Place Eval1 dom :Played*/
  array [36]Eval1 = (0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 );
  /** Place End dom :Player*/
  array [2]End = (0, 0 );
  /**Play*/
  transition Play(Player $p, Direction $d, Position $posV, Position $posH) [ Idle[ $p ] >= 1 && FreePositions[ ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ] >= 1 ] {
    Idle[ $p ] -= 1    ;
    FreePositions[ ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ] -= 1    ;
    OccupiedPositions[ ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ] += 1    ;
    Chosed[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] += 1    ;
  }
  /**Win1*/
  transition Win1(Player $p, Direction $d, Position $posV, Count $n, Bool $b, Position $posH) [ $posH <= 1 && $posV <= 1 && Chosed[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] >= 1 && IsWinner[ ( ( $p * 2 ) + $b ) ] >= 1 && Score[ ( ( $p * 10 ) + $n ) ] >= 1 && OccupiedPositions[ ( ( ( ( $d + 1 ) % 2 ) * 9 ) + ( ( $posH * 3 ) + $posV ) ) ] >= 1 && OccupiedPositions[ ( ( 1 * 9 ) + ( ( $posH * 3 ) + ( ( $posV + 1 ) % 3 ) ) ) ] >= 1 && OccupiedPositions[ ( ( 0 * 9 ) + ( ( ( ( $posH + 1 ) % 3 ) * 3 ) + $posV ) ) ] >= 1 ] {
    Chosed[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] -= 1    ;
    IsWinner[ ( ( $p * 2 ) + $b ) ] -= 1    ;
    Score[ ( ( $p * 10 ) + $n ) ] -= 1    ;
    Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] += 1    ;
    Score[ ( ( $p * 10 ) + ( ( $n + 1 ) % 10 ) ) ] += 1    ;
    IsWinner[ ( ( $p * 2 ) + 0 ) ] += 1    ;
  }
  /**Lose1*/
  transition Lose1(Player $p, Direction $d, Position $posV1, Position $posV, Direction $d1, Position $posH1, Position $posH) [ $posH <= 1 && $posV <= 1 && ( $d1 != $d && $posH1 == $posH && $posV1 == $posV || $d1 == 0 && $posH1 == ( $posH + 1 ) && $posV1 == $posV || $d1 == 1 && $posH1 == $posH && $posV1 == ( $posV + 1 ) ) && FreePositions[ ( ( $d1 * 9 ) + ( ( $posH1 * 3 ) + $posV1 ) ) ] >= 1 && Chosed[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] >= 1 ] {
    Chosed[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] -= 1    ;
    Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] += 1    ;
  }
  /**Win2H*/
  transition Win2H(Player $p, Direction $d, Position $posV, Count $n, Bool $b, Position $posH) [ $posH >= 1 && $posV <= 1 && Score[ ( ( $p * 10 ) + $n ) ] >= 1 && IsWinner[ ( ( $p * 2 ) + $b ) ] >= 1 && Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] >= 1 && OccupiedPositions[ ( ( 1 * 9 ) + ( ( ( ( ( ( $posH - 1 ) % 3 ) + 3 ) % 3 ) * 3 ) + $posV ) ) ] >= 1 && OccupiedPositions[ ( ( 0 * 9 ) + ( ( ( ( ( ( $posH - 1 ) % 3 ) + 3 ) % 3 ) * 3 ) + $posV ) ) ] >= 1 && OccupiedPositions[ ( ( 1 * 9 ) + ( ( ( ( ( ( $posH - 1 ) % 3 ) + 3 ) % 3 ) * 3 ) + ( ( $posV + 1 ) % 3 ) ) ) ] >= 1 ] {
    Score[ ( ( $p * 10 ) + $n ) ] -= 1    ;
    IsWinner[ ( ( $p * 2 ) + $b ) ] -= 1    ;
    Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] -= 1    ;
    Score[ ( ( $p * 10 ) + ( ( $n + 1 ) % 10 ) ) ] += 1    ;
    IsWinner[ ( ( $p * 2 ) + 1 ) ] += 1    ;
    Idle[ $p ] += 1    ;
  }
  /**Lose2*/
  transition Lose2(Player $p, Direction $d, Position $posV1, Position $posV, Direction $d1, Position $posH1, Position $posH) [ ( $d == 0 && $posH >= 1 && $posV <= 1 && ( $d1 == 0 && $posH1 == ( $posH - 1 ) && $posV1 == $posV || $d1 == 1 && $posH1 == ( $posH - 1 ) && $posV1 == $posV || $d1 == 1 && $posH1 == ( $posH - 1 ) && $posV1 == ( $posV + 1 ) ) || $d == 1 && $posH <= 1 && $posV >= 1 && ( $d1 == 1 && $posH1 == $posH && $posV1 == ( $posV - 1 ) || $d1 == 0 && $posH1 == $posH && $posV1 == ( $posV - 1 ) || $d1 == 0 && $posH1 == ( $posH + 1 ) && $posV1 == ( $posV - 1 ) ) ) && FreePositions[ ( ( $d1 * 9 ) + ( ( $posH1 * 3 ) + $posV1 ) ) ] >= 1 && Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] >= 1 ] {
    Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] -= 1    ;
    End[ $p ] += 1    ;
  }
  /**Win2V*/
  transition Win2V(Player $p, Direction $d, Position $posV, Count $n, Bool $b, Position $posH) [ $posH <= 1 && $posV >= 1 && Score[ ( ( $p * 10 ) + $n ) ] >= 1 && Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] >= 1 && IsWinner[ ( ( $p * 2 ) + $b ) ] >= 1 && OccupiedPositions[ ( ( 0 * 9 ) + ( ( $posH * 3 ) + ( ( ( ( $posV - 1 ) % 3 ) + 3 ) % 3 ) ) ) ] >= 1 && OccupiedPositions[ ( ( 0 * 9 ) + ( ( ( ( $posH + 1 ) % 3 ) * 3 ) + ( ( ( ( $posV - 1 ) % 3 ) + 3 ) % 3 ) ) ) ] >= 1 && OccupiedPositions[ ( ( 1 * 9 ) + ( ( $posH * 3 ) + ( ( ( ( $posV - 1 ) % 3 ) + 3 ) % 3 ) ) ) ] >= 1 ] {
    Score[ ( ( $p * 10 ) + $n ) ] -= 1    ;
    Eval1[ ( ( $p * 18 ) + ( ( $d * 9 ) + ( ( $posH * 3 ) + $posV ) ) ) ] -= 1    ;
    IsWinner[ ( ( $p * 2 ) + $b ) ] -= 1    ;
    Score[ ( ( $p * 10 ) + ( ( $n + 1 ) % 10 ) ) ] += 1    ;
    IsWinner[ ( ( $p * 2 ) + 1 ) ] += 1    ;
    Idle[ $p ] += 1    ;
  }
  /**AWin*/
  transition AWin(Player $p) [ IsWinner[ ( ( $p * 2 ) + 0 ) ] >= 1 && End[ $p ] >= 1 ] {
    IsWinner[ ( ( $p * 2 ) + 0 ) ] -= 1    ;
    End[ $p ] -= 1    ;
    Idle[ $p ] += 1    ;
    IsWinner[ ( ( $p * 2 ) + 1 ) ] += 1    ;
  }
  /**NoWin*/
  transition NoWin(Player $p) [ IsWinner[ ( ( $p * 2 ) + 1 ) ] >= 1 && End[ $p ] >= 1 ] {
    End[ $p ] -= 1    ;
    Idle[ ( ( $p + 1 ) % 2 ) ] += 1    ;
  }
}
main DotAndBoxes_COL_3 ;

property player2plays [reachable] : End[1]==1;