13 ----------------------------------------------------------------*) |
13 ----------------------------------------------------------------*) |
14 |
14 |
15 fun check(extacts,intacts,string_of_a,startsI,string_of_s, |
15 fun check(extacts,intacts,string_of_a,startsI,string_of_s, |
16 nexts,hom,transA,startsS) = |
16 nexts,hom,transA,startsS) = |
17 let fun check_s(s,unchecked,checked) = |
17 let fun check_s(s,unchecked,checked) = |
18 let fun check_sa(unchecked,a) = |
18 let fun check_sa a unchecked = |
19 let fun check_sas(unchecked,t) = |
19 let fun check_sas t unchecked = |
20 (if a mem extacts then |
20 (if a mem extacts then |
21 (if transA(hom s,a,hom t) then ( ) |
21 (if transA(hom s,a,hom t) then ( ) |
22 else (writeln("Error: Mapping of Externals!"); |
22 else (writeln("Error: Mapping of Externals!"); |
23 string_of_s s; writeln""; |
23 string_of_s s; writeln""; |
24 string_of_a a; writeln""; |
24 string_of_a a; writeln""; |
27 else (writeln("Error: Mapping of Internals!"); |
27 else (writeln("Error: Mapping of Internals!"); |
28 string_of_s s; writeln""; |
28 string_of_s s; writeln""; |
29 string_of_a a; writeln""; |
29 string_of_a a; writeln""; |
30 string_of_s t;writeln"";writeln"" )); |
30 string_of_s t;writeln"";writeln"" )); |
31 if t mem checked then unchecked else insert (op =) t unchecked) |
31 if t mem checked then unchecked else insert (op =) t unchecked) |
32 in Library.foldl check_sas (unchecked,nexts s a) end; |
32 in fold check_sas (nexts s a) unchecked end; |
33 val unchecked' = Library.foldl check_sa (unchecked,extacts @ intacts) |
33 val unchecked' = fold check_sa (extacts @ intacts) unchecked |
34 in (if s mem startsI then |
34 in (if s mem startsI then |
35 (if hom(s) mem startsS then () |
35 (if hom(s) mem startsS then () |
36 else writeln("Error: At start states!")) |
36 else writeln("Error: At start states!")) |
37 else (); |
37 else (); |
38 checks(unchecked',s::checked)) end |
38 checks(unchecked',s::checked)) end |