Przykład automatu czasowego w formacie Kronosa
(jeden z automatów otrzymanych po translacji do automatów specyfikacji protokołu alternującego bitu zapisanej w języku bazowym)

% main automaton 1
#states 8
#trans 13
#clocks 1 x1
#sync a1 a2 a3
state:0
prop: S_Sender().bit0 
invar:true
trans:
	true => a1 ; reset { x1 } ; goto 1

state:1
prop: S_Sender().bit0 
invar:x1<=2  
trans:
	x1>=2 x1<=2   => a4 ; reset { } ; goto 0
	true => a2 ; reset { } ; goto 2

state:2
prop: S_Sender().ack 
invar:true
trans:
	true => a0 ; reset { } ; goto 3

state:3
prop: 
invar:true
trans:
	true => a1 ; reset { x1 } ; goto 4

state:4
prop: 
invar:x1<=2  
trans:
	x1>=2 x1<=2   => a4 ; reset { } ; goto 3
	true => a2 ; reset { } ; goto 5
	true => a3 ; reset { } ; goto 3

state:5
prop: S_Sender().ack S_Sender().bit0 
invar:true
trans:
	true => a0 ; reset { } ; goto 6

state:6
prop: S_Sender().bit0 
invar:true
trans:
	true => a1 ; reset { x1 } ; goto 7

state:7
prop: S_Sender().bit0 
invar:x1<=2  
trans:
	x1>=2 x1<=2   => a4 ; reset { } ; goto 6
	true => a2 ; reset { } ; goto 2
	true => a3 ; reset { } ; goto 6