Minor edit

models/specification.smv

 DEFINE isDisconnected := (out=NO_CONN | out=CH_MAX | out=CH_NONE);
 DEFINE hasReqAuth := (inp=SR_AUTH & out=SR_ACCEPT);
 DEFINE hasOpenedChannel := (out=CH_OPEN_SUCCESS);
-DEFINE hasAuth := (out=UA_PK_OK | out=UA_PK_OK);
+DEFINE hasAuth := (out=UA_PK_OK | out=UA_PW_OK);
 DEFINE authReq := (inp=UA_PK_OK | inp=UA_PW_OK | inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE);