Exception in thread "main" org.scribble.ext.assrt.core.ast.AssrtCoreSyntaxException: Clock(line 20:6): [assrt-core] Unguarded in choice case: rec Clock_Lock___C__A__B_ @(")"  {
REQ(tsrab: Clock.int) from C to A; null
REQ(tsrac: Clock.int) from C to B; @(tsrac > tsrab);
choice at A {
ACK(tsaba: Clock.int) from A to C; @(tsaba > tsrab);
choice at B {
ACK(tsaca: Clock.int) from B to C; @(tsaca > tsrac);
REL(tsreab: Clock.int) from C to A; @(tsreab > tsrab);
REL(tsreac: Clock.int) from C to B; @(tsreac > tsrac);
} or {
rec Clock_Lock___B__C__A_ @(")"  {
REQ(tsrab: Clock.int) from B to C; null
REQ(tsrac: Clock.int) from B to A; @(tsrac > tsrab);
choice at C {
ACK(tsaba: Clock.int) from C to B; @(tsaba > tsrab);
choice at A {
ACK(tsaca: Clock.int) from A to B; @(tsaca > tsrac);
REL(tsreab: Clock.int) from B to C; @(tsreab > tsrab);
REL(tsreac: Clock.int) from B to A; @(tsreac > tsrac);
} or {
continue Clock_Lock___A__B__C_; @;
}
} or {
rec Clock_Lock___C__B__A_ @(")"  {
REQ(tsrab: Clock.int) from C to B; null
REQ(tsrac: Clock.int) from C to A; @(tsrac > tsrab);
choice at B {
ACK(tsaba: Clock.int) from B to C; @(tsaba > tsrab);
choice at A {
ACK(tsaca: Clock.int) from A to C; @(tsaca > tsrac);
REL(tsreab: Clock.int) from C to B; @(tsreab > tsrab);
REL(tsreac: Clock.int) from C to A; @(tsreac > tsrac);
} or {
rec Clock_Lock___A__C__B_ @(")"  {
REQ(tsrab: Clock.int) from A to C; null
REQ(tsrac: Clock.int) from A to B; @(tsrac > tsrab);
choice at C {
ACK(tsaba: Clock.int) from C to A; @(tsaba > tsrab);
choice at B {
ACK(tsaca: Clock.int) from B to A; @(tsaca > tsrac);
REL(tsreab: Clock.int) from A to C; @(tsreab > tsrab);
REL(tsreac: Clock.int) from A to B; @(tsreac > tsrac);
} or {
rec Clock_Lock___B__A__C_ @(")"  {
REQ(tsrab: Clock.int) from B to A; null
REQ(tsrac: Clock.int) from B to C; @(tsrac > tsrab);
choice at A {
ACK(tsaba: Clock.int) from A to B; @(tsaba > tsrab);
choice at C {
ACK(tsaca: Clock.int) from C to B; @(tsaca > tsrac);
REL(tsreab: Clock.int) from B to A; @(tsreab > tsrab);
REL(tsreac: Clock.int) from B to C; @(tsreac > tsrac);
} or {
continue Clock_Lock___C__B__A_; @;
}
} or {
continue Clock_Lock___A__B__C_; @;
}
}
}
} or {
continue Clock_Lock___C__A__B_; @;
}
}
}
} or {
continue Clock_Lock___B__C__A_; @;
}
}
}
}
}
} or {
rec Clock_Lock___A__C__B_ @(")"  {
REQ(tsrab: Clock.int) from A to C; null
REQ(tsrac: Clock.int) from A to B; @(tsrac > tsrab);
choice at C {
ACK(tsaba: Clock.int) from C to A; @(tsaba > tsrab);
choice at B {
ACK(tsaca: Clock.int) from B to A; @(tsaca > tsrac);
REL(tsreab: Clock.int) from A to C; @(tsreab > tsrab);
REL(tsreac: Clock.int) from A to B; @(tsreac > tsrac);
} or {
rec Clock_Lock___B__A__C_ @(")"  {
REQ(tsrab: Clock.int) from B to A; null
REQ(tsrac: Clock.int) from B to C; @(tsrac > tsrab);
choice at A {
ACK(tsaba: Clock.int) from A to B; @(tsaba > tsrab);
choice at C {
ACK(tsaca: Clock.int) from C to B; @(tsaca > tsrac);
REL(tsreab: Clock.int) from B to A; @(tsreab > tsrab);
REL(tsreac: Clock.int) from B to C; @(tsreac > tsrac);
} or {
rec Clock_Lock___C__B__A_ @(")"  {
REQ(tsrab: Clock.int) from C to B; null
REQ(tsrac: Clock.int) from C to A; @(tsrac > tsrab);
choice at B {
ACK(tsaba: Clock.int) from B to C; @(tsaba > tsrab);
choice at A {
ACK(tsaca: Clock.int) from A to C; @(tsaca > tsrac);
REL(tsreab: Clock.int) from C to B; @(tsreab > tsrab);
REL(tsreac: Clock.int) from C to A; @(tsreac > tsrac);
} or {
continue Clock_Lock___A__C__B_; @;
}
} or {
rec Clock_Lock___B__C__A_ @(")"  {
REQ(tsrab: Clock.int) from B to C; null
REQ(tsrac: Clock.int) from B to A; @(tsrac > tsrab);
choice at C {
ACK(tsaba: Clock.int) from C to B; @(tsaba > tsrab);
choice at A {
ACK(tsaca: Clock.int) from A to B; @(tsaca > tsrac);
REL(tsreab: Clock.int) from B to C; @(tsreab > tsrab);
REL(tsreac: Clock.int) from B to A; @(tsreac > tsrac);
} or {
continue Clock_Lock___A__B__C_; @;
}
} or {
continue Clock_Lock___C__B__A_; @;
}
}
}
}
}
} or {
continue Clock_Lock___A__B__C_; @;
}
}
}
} or {
continue Clock_Lock___C__A__B_; @;
}
}
}
}
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseSeq(AssrtCoreGProtocolDeclTranslator.java:131)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseGChoice(AssrtCoreGProtocolDeclTranslator.java:163)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseSeq(AssrtCoreGProtocolDeclTranslator.java:140)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseGSimpleInteractionNode(AssrtCoreGProtocolDeclTranslator.java:293)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseAssrtGMessageTransfer(AssrtCoreGProtocolDeclTranslator.java:266)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseSeq(AssrtCoreGProtocolDeclTranslator.java:108)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseGChoice(AssrtCoreGProtocolDeclTranslator.java:163)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseSeq(AssrtCoreGProtocolDeclTranslator.java:140)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseGSimpleInteractionNode(AssrtCoreGProtocolDeclTranslator.java:293)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseAssrtGMessageTransfer(AssrtCoreGProtocolDeclTranslator.java:266)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseSeq(AssrtCoreGProtocolDeclTranslator.java:108)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseGSimpleInteractionNode(AssrtCoreGProtocolDeclTranslator.java:293)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseAssrtGMessageTransfer(AssrtCoreGProtocolDeclTranslator.java:266)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseSeq(AssrtCoreGProtocolDeclTranslator.java:108)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseAssrtGRecursion(AssrtCoreGProtocolDeclTranslator.java:223)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.parseSeq(AssrtCoreGProtocolDeclTranslator.java:144)
	at org.scribble.ext.assrt.core.ast.global.AssrtCoreGProtocolDeclTranslator.translate(AssrtCoreGProtocolDeclTranslator.java:91)
	at org.scribble.ext.assrt.cli.AssrtCommandLine.assrtCoreParseAndCheckWF(AssrtCommandLine.java:184)
	at org.scribble.ext.assrt.cli.AssrtCommandLine.doAssrtCoreValidationTasks(AssrtCommandLine.java:141)
	at org.scribble.ext.assrt.cli.AssrtCommandLine.doValidationTasks(AssrtCommandLine.java:116)
	at org.scribble.cli.CommandLine.runBody(CommandLine.java:145)
	at org.scribble.cli.CommandLine.run(CommandLine.java:108)
	at org.scribble.ext.assrt.cli.AssrtCommandLine.main(AssrtCommandLine.java:108)



module Clock;

type <java> "java.lang.Integer" from "rt.jar" as int;

global protocol Lock(role A, role B, role C)
{
	REQ (tsrab:int) from A to B;
	REQ (tsrac:int) from A to C; @"tsrac > tsrab"
	choice at B
	{
		ACK (tsaba:int) from B to A; @"tsaba >  tsrab"
		choice at C
		{
			ACK (tsaca:int) from C to A; @"tsaca > tsrac"
			REL (tsreab:int) from A to B; @"tsreab > tsrab"
			REL (tsreac:int) from A to C; @"tsreac > tsrac"
		}
		or
		{
			do Lock(C, A, B);
		}

	}
	or
	{
		do Lock(B, A, C); // should we set the initial clocks here?
	}
}