:: Minimization of finite state machines
:: by Miroslava Kaloper and Piotr Rudnicki
::
:: Received November 18, 1994
:: Copyright (c) 1994 Association of Mizar Users
theorem Th1: :: FSM_1:1
theorem :: FSM_1:2
canceled;
theorem :: FSM_1:3
canceled;
theorem :: FSM_1:4
canceled;
theorem :: FSM_1:5
canceled;
theorem :: FSM_1:6
canceled;
theorem Th7: :: FSM_1:7
theorem Th8: :: FSM_1:8
theorem :: FSM_1:9
theorem :: FSM_1:10
theorem Th11: :: FSM_1:11
theorem Th12: :: FSM_1:12
theorem Th13: :: FSM_1:13
theorem Th14: :: FSM_1:14
theorem Th15: :: FSM_1:15
:: deftheorem defines -succ_of FSM_1:def 1 :
:: deftheorem Def2 defines -admissible FSM_1:def 2 :
theorem Th16: :: FSM_1:16
:: deftheorem Def3 defines -leads_to FSM_1:def 3 :
theorem Th17: :: FSM_1:17
:: deftheorem Def4 defines is_admissible_for FSM_1:def 4 :
theorem :: FSM_1:18
:: deftheorem Def5 defines leads_to_under FSM_1:def 5 :
theorem Th19: :: FSM_1:19
theorem Th20: :: FSM_1:20
theorem Th21: :: FSM_1:21
theorem Th22: :: FSM_1:22
theorem Th23: :: FSM_1:23
definition
let IAlph be
set ;
let OAlph be non
empty set ;
attr c3 is
strict;
struct Mealy-FSM of
IAlph,
OAlph -> FSM of
IAlph;
aggr Mealy-FSM(#
carrier,
Tran,
OFun,
InitS #)
-> Mealy-FSM of
IAlph,
OAlph;
sel OFun c3 -> Function of
[:the carrier of c3,IAlph:],
OAlph;
attr c3 is
strict;
struct Moore-FSM of
IAlph,
OAlph -> FSM of
IAlph;
aggr Moore-FSM(#
carrier,
Tran,
OFun,
InitS #)
-> Moore-FSM of
IAlph,
OAlph;
sel OFun c3 -> Function of the
carrier of
c3,
OAlph;
end;
registration
let IAlph be
set ;
let OAlph be non
empty set ;
let X be non
empty finite set ;
let T be
Function of
[:X,IAlph:],
X;
let O be
Function of
[:X,IAlph:],
OAlph;
let I be
Element of
X;
cluster Mealy-FSM(#
X,
T,
O,
I #)
-> non
empty finite ;
coherence
( Mealy-FSM(# X,T,O,I #) is finite & not Mealy-FSM(# X,T,O,I #) is empty )
;
end;
registration
let IAlph be
set ;
let OAlph be non
empty set ;
let X be non
empty finite set ;
let T be
Function of
[:X,IAlph:],
X;
let O be
Function of
X,
OAlph;
let I be
Element of
X;
cluster Moore-FSM(#
X,
T,
O,
I #)
-> non
empty finite ;
coherence
( Moore-FSM(# X,T,O,I #) is finite & not Moore-FSM(# X,T,O,I #) is empty )
;
end;
definition
let IAlph,
OAlph be non
empty set ;
let tfsm be non
empty Mealy-FSM of
IAlph,
OAlph;
let qt be
State of
tfsm;
let w be
FinSequence of
IAlph;
func qt,
w -response -> FinSequence of
OAlph means :
Def6:
:: FSM_1:def 6
(
len it = len w & ( for
i being
Element of
NAT st
i in dom w holds
it . i = the
OFun of
tfsm . [((qt,w -admissible ) . i),(w . i)] ) );
existence
ex b1 being FinSequence of OAlph st
( len b1 = len w & ( for i being Element of NAT st i in dom w holds
b1 . i = the OFun of tfsm . [((qt,w -admissible ) . i),(w . i)] ) )
uniqueness
for b1, b2 being FinSequence of OAlph st len b1 = len w & ( for i being Element of NAT st i in dom w holds
b1 . i = the OFun of tfsm . [((qt,w -admissible ) . i),(w . i)] ) & len b2 = len w & ( for i being Element of NAT st i in dom w holds
b2 . i = the OFun of tfsm . [((qt,w -admissible ) . i),(w . i)] ) holds
b1 = b2
end;
:: deftheorem Def6 defines -response FSM_1:def 6 :
theorem Th24: :: FSM_1:24
:: deftheorem Def7 defines -response FSM_1:def 7 :
theorem Th25: :: FSM_1:25
theorem Th26: :: FSM_1:26
theorem Th27: :: FSM_1:27
for
IAlph,
OAlph being non
empty set for
w1,
w2 being
FinSequence of
IAlph for
tfsm1,
tfsm2 being non
empty Mealy-FSM of
IAlph,
OAlph for
q11,
q12 being
State of
tfsm1 for
q21,
q22 being
State of
tfsm2 st
q11,
w1 -leads_to q12 &
q21,
w1 -leads_to q22 &
q12,
w2 -response <> q22,
w2 -response holds
q11,
(w1 ^ w2) -response <> q21,
(w1 ^ w2) -response
:: deftheorem defines is_similar_to FSM_1:def 8 :
theorem :: FSM_1:28
theorem :: FSM_1:29
definition
let IAlph,
OAlph be non
empty set ;
let tfsm1,
tfsm2 be non
empty Mealy-FSM of
IAlph,
OAlph;
pred tfsm1,
tfsm2 -are_equivalent means :
Def9:
:: FSM_1:def 9
for
w being
FinSequence of
IAlph holds the
InitS of
tfsm1,
w -response = the
InitS of
tfsm2,
w -response ;
reflexivity
for tfsm1 being non empty Mealy-FSM of IAlph,OAlph
for w being FinSequence of IAlph holds the InitS of tfsm1,w -response = the InitS of tfsm1,w -response
;
symmetry
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph st ( for w being FinSequence of IAlph holds the InitS of tfsm1,w -response = the InitS of tfsm2,w -response ) holds
for w being FinSequence of IAlph holds the InitS of tfsm2,w -response = the InitS of tfsm1,w -response
;
end;
:: deftheorem Def9 defines -are_equivalent FSM_1:def 9 :
theorem Th30: :: FSM_1:30
definition
let IAlph,
OAlph be non
empty set ;
let tfsm be non
empty Mealy-FSM of
IAlph,
OAlph;
let qa,
qb be
State of
tfsm;
pred qa,
qb -are_equivalent means :
Def10:
:: FSM_1:def 10
for
w being
FinSequence of
IAlph holds
qa,
w -response = qb,
w -response ;
reflexivity
for qa being State of tfsm
for w being FinSequence of IAlph holds qa,w -response = qa,w -response
;
symmetry
for qa, qb being State of tfsm st ( for w being FinSequence of IAlph holds qa,w -response = qb,w -response ) holds
for w being FinSequence of IAlph holds qb,w -response = qa,w -response
;
end;
:: deftheorem Def10 defines -are_equivalent FSM_1:def 10 :
theorem :: FSM_1:31
canceled;
theorem :: FSM_1:32
canceled;
theorem :: FSM_1:33
theorem Th34: :: FSM_1:34
theorem Th35: :: FSM_1:35
theorem Th36: :: FSM_1:36
theorem :: FSM_1:37
:: deftheorem Def11 defines -equivalent FSM_1:def 11 :
theorem Th38: :: FSM_1:38
theorem Th39: :: FSM_1:39
theorem Th40: :: FSM_1:40
theorem Th41: :: FSM_1:41
theorem Th42: :: FSM_1:42
theorem Th43: :: FSM_1:43
theorem Th44: :: FSM_1:44
definition
let IAlph,
OAlph be non
empty set ;
let tfsm be non
empty Mealy-FSM of
IAlph,
OAlph;
let i be
Nat;
func i -eq_states_EqR tfsm -> Equivalence_Relation of the
carrier of
tfsm means :
Def12:
:: FSM_1:def 12
for
qa,
qb being
State of
tfsm holds
(
[qa,qb] in it iff
i -equivalent qa,
qb );
existence
ex b1 being Equivalence_Relation of the carrier of tfsm st
for qa, qb being State of tfsm holds
( [qa,qb] in b1 iff i -equivalent qa,qb )
uniqueness
for b1, b2 being Equivalence_Relation of the carrier of tfsm st ( for qa, qb being State of tfsm holds
( [qa,qb] in b1 iff i -equivalent qa,qb ) ) & ( for qa, qb being State of tfsm holds
( [qa,qb] in b2 iff i -equivalent qa,qb ) ) holds
b1 = b2
end;
:: deftheorem Def12 defines -eq_states_EqR FSM_1:def 12 :
:: deftheorem defines -eq_states_partition FSM_1:def 13 :
theorem Th45: :: FSM_1:45
theorem Th46: :: FSM_1:46
theorem :: FSM_1:47
theorem Th48: :: FSM_1:48
theorem Th49: :: FSM_1:49
theorem Th50: :: FSM_1:50
theorem :: FSM_1:51
theorem Th52: :: FSM_1:52
:: deftheorem Def14 defines final FSM_1:def 14 :
theorem :: FSM_1:53
theorem Th54: :: FSM_1:54
theorem :: FSM_1:55
:: deftheorem Def15 defines final_states_partition FSM_1:def 15 :
theorem Th56: :: FSM_1:56
definition
let IAlph,
OAlph be non
empty set ;
let tfsm be non
empty finite Mealy-FSM of
IAlph,
OAlph;
let qf be
Element of
final_states_partition tfsm;
let s be
Element of
IAlph;
func s,
qf -succ_class -> Element of
final_states_partition tfsm means :
Def16:
:: FSM_1:def 16
ex
q being
State of
tfsm ex
n being
Element of
NAT st
(
q in qf &
n + 1
= card the
carrier of
tfsm &
it = Class (n -eq_states_EqR tfsm),
(the Tran of tfsm . [q,s]) );
existence
ex b1 being Element of final_states_partition tfsm ex q being State of tfsm ex n being Element of NAT st
( q in qf & n + 1 = card the carrier of tfsm & b1 = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) )
uniqueness
for b1, b2 being Element of final_states_partition tfsm st ex q being State of tfsm ex n being Element of NAT st
( q in qf & n + 1 = card the carrier of tfsm & b1 = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) ) & ex q being State of tfsm ex n being Element of NAT st
( q in qf & n + 1 = card the carrier of tfsm & b2 = Class (n -eq_states_EqR tfsm),(the Tran of tfsm . [q,s]) ) holds
b1 = b2
end;
:: deftheorem Def16 defines -succ_class FSM_1:def 16 :
:: deftheorem Def17 defines -class_response FSM_1:def 17 :
definition
let IAlph,
OAlph be non
empty set ;
let tfsm be non
empty finite Mealy-FSM of
IAlph,
OAlph;
func the_reduction_of tfsm -> strict Mealy-FSM of
IAlph,
OAlph means :
Def18:
:: FSM_1:def 18
( the
carrier of
it = final_states_partition tfsm & ( for
Q being
State of
it for
s being
Element of
IAlph for
q being
State of
tfsm st
q in Q holds
( the
Tran of
tfsm . q,
s in the
Tran of
it . Q,
s & the
OFun of
tfsm . q,
s = the
OFun of
it . Q,
s ) ) & the
InitS of
tfsm in the
InitS of
it );
existence
ex b1 being strict Mealy-FSM of IAlph,OAlph st
( the carrier of b1 = final_states_partition tfsm & ( for Q being State of b1
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . q,s in the Tran of b1 . Q,s & the OFun of tfsm . q,s = the OFun of b1 . Q,s ) ) & the InitS of tfsm in the InitS of b1 )
uniqueness
for b1, b2 being strict Mealy-FSM of IAlph,OAlph st the carrier of b1 = final_states_partition tfsm & ( for Q being State of b1
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . q,s in the Tran of b1 . Q,s & the OFun of tfsm . q,s = the OFun of b1 . Q,s ) ) & the InitS of tfsm in the InitS of b1 & the carrier of b2 = final_states_partition tfsm & ( for Q being State of b2
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . q,s in the Tran of b2 . Q,s & the OFun of tfsm . q,s = the OFun of b2 . Q,s ) ) & the InitS of tfsm in the InitS of b2 holds
b1 = b2
end;
:: deftheorem Def18 defines the_reduction_of FSM_1:def 18 :
theorem Th57: :: FSM_1:57
theorem Th58: :: FSM_1:58
definition
let IAlph,
OAlph be non
empty set ;
let tfsm1,
tfsm2 be non
empty Mealy-FSM of
IAlph,
OAlph;
pred tfsm1,
tfsm2 -are_isomorphic means :
Def19:
:: FSM_1:def 19
ex
Tf being
Function of the
carrier of
tfsm1,the
carrier of
tfsm2 st
(
Tf is
bijective &
Tf . the
InitS of
tfsm1 = the
InitS of
tfsm2 & ( for
q11 being
State of
tfsm1 for
s being
Element of
IAlph holds
(
Tf . (the Tran of tfsm1 . q11,s) = the
Tran of
tfsm2 . (Tf . q11),
s & the
OFun of
tfsm1 . q11,
s = the
OFun of
tfsm2 . (Tf . q11),
s ) ) );
reflexivity
for tfsm1 being non empty Mealy-FSM of IAlph,OAlph ex Tf being Function of the carrier of tfsm1,the carrier of tfsm1 st
( Tf is bijective & Tf . the InitS of tfsm1 = the InitS of tfsm1 & ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm1 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm1 . (Tf . q11),s ) ) )
symmetry
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph st ex Tf being Function of the carrier of tfsm1,the carrier of tfsm2 st
( Tf is bijective & Tf . the InitS of tfsm1 = the InitS of tfsm2 & ( for q11 being State of tfsm1
for s being Element of IAlph holds
( Tf . (the Tran of tfsm1 . q11,s) = the Tran of tfsm2 . (Tf . q11),s & the OFun of tfsm1 . q11,s = the OFun of tfsm2 . (Tf . q11),s ) ) ) holds
ex Tf being Function of the carrier of tfsm2,the carrier of tfsm1 st
( Tf is bijective & Tf . the InitS of tfsm2 = the InitS of tfsm1 & ( for q11 being State of tfsm2
for s being Element of IAlph holds
( Tf . (the Tran of tfsm2 . q11,s) = the Tran of tfsm1 . (Tf . q11),s & the OFun of tfsm2 . q11,s = the OFun of tfsm1 . (Tf . q11),s ) ) )
end;
:: deftheorem Def19 defines -are_isomorphic FSM_1:def 19 :
theorem Th59: :: FSM_1:59
theorem Th60: :: FSM_1:60
theorem Th61: :: FSM_1:61
for
OAlph,
IAlph being non
empty set for
tfsm1,
tfsm2 being non
empty Mealy-FSM of
IAlph,
OAlph for
q11,
q12 being
State of
tfsm1 for
Tf being
Function of the
carrier of
tfsm1,the
carrier of
tfsm2 st
Tf . the
InitS of
tfsm1 = the
InitS of
tfsm2 & ( for
q being
State of
tfsm1 for
s being
Element of
IAlph holds
(
Tf . (the Tran of tfsm1 . q,s) = the
Tran of
tfsm2 . (Tf . q),
s & the
OFun of
tfsm1 . q,
s = the
OFun of
tfsm2 . (Tf . q),
s ) ) holds
(
q11,
q12 -are_equivalent iff
Tf . q11,
Tf . q12 -are_equivalent )
theorem Th62: :: FSM_1:62
:: deftheorem Def20 defines reduced FSM_1:def 20 :
theorem Th63: :: FSM_1:63
theorem Th64: :: FSM_1:64
theorem Th65: :: FSM_1:65
:: deftheorem Def21 defines accessible FSM_1:def 21 :
:: deftheorem Def22 defines connected FSM_1:def 22 :
theorem Th66: :: FSM_1:66
:: deftheorem defines accessibleStates FSM_1:def 23 :
theorem Th67: :: FSM_1:67
theorem Th68: :: FSM_1:68
theorem :: FSM_1:69
for
IAlph,
OAlph being non
empty set for
tfsm being non
empty finite Mealy-FSM of
IAlph,
OAlph for
cTran being
Function of
[:(accessibleStates tfsm),IAlph:],
accessibleStates tfsm for
cOFun being
Function of
[:(accessibleStates tfsm),IAlph:],
OAlph for
cInitS being
Element of
accessibleStates tfsm st
cTran = the
Tran of
tfsm | [:(accessibleStates tfsm),IAlph:] &
cOFun = the
OFun of
tfsm | [:(accessibleStates tfsm),IAlph:] &
cInitS = the
InitS of
tfsm holds
tfsm,
Mealy-FSM(#
(accessibleStates tfsm),
cTran,
cOFun,
cInitS #)
-are_equivalent
theorem :: FSM_1:70
:: deftheorem Def24 defines -Mealy_union FSM_1:def 24 :
theorem Th71: :: FSM_1:71
theorem Th72: :: FSM_1:72
theorem Th73: :: FSM_1:73
theorem Th74: :: FSM_1:74
theorem Th75: :: FSM_1:75
theorem Th76: :: FSM_1:76
theorem Th77: :: FSM_1:77
theorem Th78: :: FSM_1:78
theorem Th79: :: FSM_1:79
theorem Th80: :: FSM_1:80
theorem Th81: :: FSM_1:81
theorem Th82: :: FSM_1:82
theorem Th83: :: FSM_1:83
theorem Th84: :: FSM_1:84
theorem :: FSM_1:85