Question Cubicle
Page 1 sur 1
Question Cubicle
Je bloque dès la question 1 sur Cubicle. Comment on fait pour prouver une propriété de liveness comme ce qui est demandé ? Je ne trouve rien là-dessus.
robinm- Messages : 4
Date d'inscription : 18/02/2017
Re: Question Cubicle
Okay je pense avoir trouvé, en utilisant Stop et la condition du while :
unsafe (i j) { PC[j] = Stop && not ( Want[Other[i]] && Turn <> i) }
Mais il me crache une erreur de syntaxe peu importe comment je le tourne :
unsafe (i j) { PC[j] = Stop && (Want[j] = False || Turn = i) } ça passe pas non plus (il aime pas le || apparemment)
unsafe (i j) { PC[j] = Stop && not ( Want[Other[i]] && Turn <> i) }
Mais il me crache une erreur de syntaxe peu importe comment je le tourne :
unsafe (i j) { PC[j] = Stop && (Want[j] = False || Turn = i) } ça passe pas non plus (il aime pas le || apparemment)
robinm- Messages : 4
Date d'inscription : 18/02/2017
Re: Question Cubicle
jsuis con c'est pas un "not".
bon, du coup ça colle avec le parser de cubicle : unsafe (i j) { PC[j] = Stop && Want[j] = True && Turn <> i }
bon, du coup ça colle avec le parser de cubicle : unsafe (i j) { PC[j] = Stop && Want[j] = True && Turn <> i }
robinm- Messages : 4
Date d'inscription : 18/02/2017
Page 1 sur 1
Permission de ce forum:
Vous ne pouvez pas répondre aux sujets dans ce forum