atm_automata/
atm_automata.rs

1/// Example: Build and display an automaton (ATM protocol)
2use rust_lstar::{
3    automata::{automata, transition},
4    *,
5};
6
7fn add_transition(
8    transitions: &mut Vec<Transition>,
9    counter: &mut usize,
10    src: &State,
11    dst: &State,
12    i: &Letter,
13    o: &Letter,
14) {
15    transitions.push(transition::Transition::new_with_source(
16        counter.to_string(),
17        src.name.clone(),
18        dst.clone(),
19        i.clone(),
20        o.clone(),
21    ));
22    *counter += 1;
23}
24
25fn main() -> Result<(), Box<dyn std::error::Error>> {
26    // Create states
27    let mut states = vec![
28        State::new("0".to_string()),
29        State::new("1".to_string()),
30        State::new("2".to_string()),
31        State::new("3".to_string()),
32        State::new("4".to_string()),
33    ];
34
35    // create vector of input letters
36    let input_letters = vec![
37        Letter::new("INSERT_CARD".to_string()),
38        Letter::new("ENTER_PIN".to_string()),
39        Letter::new("REQUEST_WITHDRAW".to_string()),
40        Letter::new("EJECT_CARD".to_string()),
41        Letter::new("TIMEOUT".to_string()),
42    ];
43
44    // create vector of output letter
45    let output_letters = vec![
46        Letter::new("CARD_ACCEPTED".to_string()),
47        Letter::new("INVALID_OP".to_string()),
48        Letter::new("RETRY".to_string()),
49        Letter::new("PIN_VERIFIED".to_string()),
50        Letter::new("CARD_EJECTED".to_string()),
51        Letter::new("INVALID_COMMAND".to_string()),
52        Letter::new("ENTER_AMOUNT".to_string()),
53        Letter::new("DISPENSING".to_string()),
54        Letter::new("WAIT".to_string()),
55        Letter::new("SESSION_TIMEOUT".to_string()),
56    ];
57
58    // create vector of transitions
59    let mut transitions: Vec<Transition> = Vec::new();
60    let mut counter: usize = 0;
61    // Transitions (from the provided DOT)
62    add_transition(
63        &mut transitions,
64        &mut counter,
65        &states[0],
66        &states[1],
67        &input_letters[0],
68        &output_letters[0],
69    );
70    add_transition(
71        &mut transitions,
72        &mut counter,
73        &states[0],
74        &states[0],
75        &input_letters[1],
76        &output_letters[3],
77    );
78    add_transition(
79        &mut transitions,
80        &mut counter,
81        &states[0],
82        &states[0],
83        &input_letters[2],
84        &output_letters[1],
85    );
86    add_transition(
87        &mut transitions,
88        &mut counter,
89        &states[0],
90        &states[0],
91        &input_letters[3],
92        &output_letters[2],
93    );
94    add_transition(
95        &mut transitions,
96        &mut counter,
97        &states[0],
98        &states[0],
99        &input_letters[4],
100        &output_letters[1],
101    );
102    states[0].transitions = transitions[0..5].to_vec();
103
104    add_transition(
105        &mut transitions,
106        &mut counter,
107        &states[1],
108        &states[1],
109        &input_letters[0],
110        &output_letters[2],
111    );
112    add_transition(
113        &mut transitions,
114        &mut counter,
115        &states[1],
116        &states[2],
117        &input_letters[1],
118        &output_letters[3],
119    );
120    add_transition(
121        &mut transitions,
122        &mut counter,
123        &states[1],
124        &states[1],
125        &input_letters[2],
126        &output_letters[2],
127    );
128    add_transition(
129        &mut transitions,
130        &mut counter,
131        &states[1],
132        &states[0],
133        &input_letters[3],
134        &output_letters[4],
135    );
136    add_transition(
137        &mut transitions,
138        &mut counter,
139        &states[1],
140        &states[1],
141        &input_letters[4],
142        &output_letters[2],
143    );
144    states[1].transitions = transitions[5..10].to_vec();
145
146    add_transition(
147        &mut transitions,
148        &mut counter,
149        &states[2],
150        &states[2],
151        &input_letters[0],
152        &output_letters[5],
153    );
154    add_transition(
155        &mut transitions,
156        &mut counter,
157        &states[2],
158        &states[2],
159        &input_letters[1],
160        &output_letters[5],
161    );
162    add_transition(
163        &mut transitions,
164        &mut counter,
165        &states[2],
166        &states[3],
167        &input_letters[2],
168        &output_letters[6],
169    );
170    add_transition(
171        &mut transitions,
172        &mut counter,
173        &states[2],
174        &states[0],
175        &input_letters[3],
176        &output_letters[4],
177    );
178    add_transition(
179        &mut transitions,
180        &mut counter,
181        &states[2],
182        &states[0],
183        &input_letters[4],
184        &output_letters[9],
185    );
186    states[2].transitions = transitions[10..15].to_vec();
187
188    add_transition(
189        &mut transitions,
190        &mut counter,
191        &states[3],
192        &states[3],
193        &input_letters[0],
194        &output_letters[8],
195    );
196    add_transition(
197        &mut transitions,
198        &mut counter,
199        &states[3],
200        &states[3],
201        &input_letters[1],
202        &output_letters[8],
203    );
204    add_transition(
205        &mut transitions,
206        &mut counter,
207        &states[3],
208        &states[4],
209        &input_letters[2],
210        &output_letters[7],
211    );
212    add_transition(
213        &mut transitions,
214        &mut counter,
215        &states[3],
216        &states[0],
217        &input_letters[3],
218        &output_letters[4],
219    );
220    add_transition(
221        &mut transitions,
222        &mut counter,
223        &states[3],
224        &states[3],
225        &input_letters[4],
226        &output_letters[7],
227    );
228    states[3].transitions = transitions[15..20].to_vec();
229
230    add_transition(
231        &mut transitions,
232        &mut counter,
233        &states[4],
234        &states[4],
235        &input_letters[0],
236        &output_letters[7],
237    );
238    add_transition(
239        &mut transitions,
240        &mut counter,
241        &states[4],
242        &states[4],
243        &input_letters[1],
244        &output_letters[7],
245    );
246    add_transition(
247        &mut transitions,
248        &mut counter,
249        &states[4],
250        &states[4],
251        &input_letters[2],
252        &output_letters[7],
253    );
254    add_transition(
255        &mut transitions,
256        &mut counter,
257        &states[4],
258        &states[0],
259        &input_letters[3],
260        &output_letters[4],
261    );
262    add_transition(
263        &mut transitions,
264        &mut counter,
265        &states[4],
266        &states[4],
267        &input_letters[4],
268        &output_letters[7],
269    );
270    states[4].transitions = transitions[20..25].to_vec();
271
272    // add("0", "1", "INSERT_CARD", "CARD_ACCEPTED");
273    // add("0", "0", "ENTER_PIN", "INVALID_OP");
274    // add("0", "0", "REQUEST_WITHDRAW", "INVALID_OP");
275    // add("0", "0", "EJECT_CARD", "INVALID_OP");
276    // add("0", "0", "TIMEOUT", "INVALID_OP");
277
278    // add("1", "1", "INSERT_CARD", "RETRY");
279    // add("1", "2", "ENTER_PIN", "PIN_VERIFIED");
280    // add("1", "1", "REQUEST_WITHDRAW", "RETRY");
281    // add("1", "0", "EJECT_CARD", "CARD_EJECTED");
282    // add("1", "1", "TIMEOUT", "RETRY");
283
284    // add("4", "4", "INSERT_CARD", "DISPENSING");
285    // add("4", "4", "ENTER_PIN", "DISPENSING");
286    // add("4", "4", "REQUEST_WITHDRAW", "DISPENSING");
287    // add("4", "0", "EJECT_CARD", "CARD_EJECTED");
288    // add("4", "4", "TIMEOUT", "DISPENSING");
289
290    // add("2", "2", "INSERT_CARD", "INVALID_COMMAND");
291    // add("2", "2", "ENTER_PIN", "INVALID_COMMAND");
292    // add("2", "3", "REQUEST_WITHDRAW", "ENTER_AMOUNT");
293    // add("2", "0", "EJECT_CARD", "CARD_EJECTED");
294    // add("2", "0", "TIMEOUT", "SESSION_TIMEOUT");
295
296    // add("3", "3", "INSERT_CARD", "WAIT");
297    // add("3", "3", "ENTER_PIN", "WAIT");
298    // add("3", "4", "REQUEST_WITHDRAW", "DISPENSING");
299    // add("3", "0", "EJECT_CARD", "CARD_EJECTED");
300    // add("3", "3", "TIMEOUT", "WAIT");
301
302    let mut automaton = automata::Automata::new(states[0].clone(), "ATM".to_string());
303    automaton.transitions = transitions.clone();
304    // Print DOT
305    println!("{}", automaton.build_dot_code());
306
307    Ok(())
308}
atm_automata/atm_automata.rs

atm_automata/
atm_automata.rs
