1use super::{
2 Action, Channel, ChannelSystem, Clock, CsError, Location, Message, PgError, PgExpression, PgId,
3 ProgramGraphBuilder, Var,
4};
5use crate::channel_system::ChannelCapacity;
6use crate::grammar::{BooleanExpr, Type};
7use crate::program_graph::ProgramGraph;
8use crate::{Expression, TimeRange, Val};
9use get_size2::GetSize;
10use log::info;
11use std::collections::BTreeMap;
12
13pub type CsExpression = Expression<Var>;
15
16pub type CsGuard = BooleanExpr<Var>;
18
19impl From<(PgId, CsExpression)> for PgExpression {
22 fn from((pg_id, expr): (PgId, CsExpression)) -> Self {
23 expr.map(&|cs_var: Var| {
24 assert_eq!(cs_var.0, pg_id);
25 cs_var.1
26 })
27 }
28}
29
30pub struct ChannelSystemBuilder {
32 program_graphs: Vec<ProgramGraphBuilder>,
33 channels: Vec<(Vec<Type>, ChannelCapacity)>,
34 communications: BTreeMap<Action, Option<(Channel, Message)>>,
35}
36
37impl Default for ChannelSystemBuilder {
38 fn default() -> Self {
39 Self::new()
40 }
41}
42
43impl ChannelSystemBuilder {
44 pub fn new() -> Self {
47 Self {
48 program_graphs: Vec::new(),
49 channels: Vec::new(),
50 communications: BTreeMap::new(),
51 }
52 }
53
54 pub fn new_program_graph(&mut self) -> PgId {
56 let pg_id = PgId(self.program_graphs.len() as u16);
57 let pg = ProgramGraphBuilder::new();
58 self.program_graphs.push(pg);
59 pg_id
60 }
61
62 pub fn new_var(&mut self, pg_id: PgId, val: Val) -> Result<Var, CsError> {
68 let pg = self
69 .program_graphs
70 .get_mut(pg_id.0 as usize)
71 .ok_or(CsError::MissingPg(pg_id))?;
72 let var = pg.new_var(val);
73 Ok(Var(pg_id, var))
74 }
75
76 pub fn new_clock(&mut self, pg_id: PgId) -> Result<Clock, CsError> {
82 self.program_graphs
83 .get_mut(pg_id.0 as usize)
84 .ok_or(CsError::MissingPg(pg_id))
85 .map(|pg| Clock(pg_id, pg.new_clock()))
86 }
87
88 pub fn new_action(&mut self, pg_id: PgId) -> Result<Action, CsError> {
94 self.program_graphs
95 .get_mut(pg_id.0 as usize)
96 .ok_or(CsError::MissingPg(pg_id))
97 .map(|pg| Action(pg_id, pg.new_action()))
98 .inspect(|&action| {
99 self.communications.insert(action, None);
100 })
101 }
102
103 pub fn add_reset(&mut self, pg_id: PgId, action: Action, clock: Clock) -> Result<(), CsError> {
110 if action.0 != pg_id {
111 return Err(CsError::ActionNotInPg(action, pg_id));
112 }
113 if clock.0 != pg_id {
114 return Err(CsError::ClockNotInPg(clock, pg_id));
115 }
116 self.program_graphs
117 .get_mut(pg_id.0 as usize)
118 .ok_or(CsError::MissingPg(pg_id))
119 .and_then(|pg| {
120 pg.add_reset(action.1, clock.1)
121 .map_err(|err| CsError::ProgramGraph(pg_id, err))
122 })
123 }
124
125 pub fn add_effect(
162 &mut self,
163 pg_id: PgId,
164 action: Action,
165 var: Var,
166 effect: CsExpression,
167 ) -> Result<(), CsError> {
168 if action.0 != pg_id {
169 Err(CsError::ActionNotInPg(action, pg_id))
170 } else if var.0 != pg_id {
171 Err(CsError::VarNotInPg(var, pg_id))
172 } else if self
173 .communications
174 .get(&action)
175 .ok_or(CsError::ProgramGraph(
176 action.0,
177 PgError::MissingAction(action.1),
178 ))?
179 .is_some()
180 {
181 Err(CsError::ActionIsCommunication(action))
183 } else {
184 let effect = PgExpression::from((pg_id, effect));
185 self.program_graphs
186 .get_mut(pg_id.0 as usize)
187 .ok_or(CsError::MissingPg(pg_id))
188 .and_then(|pg| {
189 pg.add_effect(action.1, var.1, effect)
190 .map_err(|err| CsError::ProgramGraph(pg_id, err))
191 })
192 }
193 }
194
195 pub fn new_location(&mut self, pg_id: PgId) -> Result<Location, CsError> {
201 self.program_graphs
202 .get_mut(pg_id.0 as usize)
203 .ok_or(CsError::MissingPg(pg_id))
204 .map(|pg| Location(pg_id, pg.new_location()))
205 }
206
207 pub fn new_timed_location(
214 &mut self,
215 pg_id: PgId,
216 invariants: &[(Clock, TimeRange)],
217 ) -> Result<Location, CsError> {
218 let invariants = invariants
219 .iter()
220 .map(|(c, range)| {
221 if c.0 == pg_id {
222 Ok((c.1, *range))
223 } else {
224 Err(CsError::DifferentPgs(pg_id, c.0))
225 }
226 })
227 .collect::<Result<Vec<_>, CsError>>()?;
228 self.program_graphs
229 .get_mut(pg_id.0 as usize)
230 .ok_or(CsError::MissingPg(pg_id))
231 .and_then(|pg| {
232 pg.new_timed_location(invariants)
233 .map(|loc| Location(pg_id, loc))
234 .map_err(|err| CsError::ProgramGraph(pg_id, err))
235 })
236 }
237
238 pub fn new_process(&mut self, pg_id: PgId, location: Location) -> Result<(), CsError> {
244 if location.0 != pg_id {
245 Err(CsError::LocationNotInPg(location, pg_id))
246 } else {
247 self.program_graphs
248 .get_mut(pg_id.0 as usize)
249 .ok_or(CsError::MissingPg(pg_id))
250 .and_then(|pg| {
251 pg.new_process(location.1)
252 .map_err(|err| CsError::ProgramGraph(pg_id, err))
253 })
254 }
255 }
256
257 pub fn new_initial_location(&mut self, pg_id: PgId) -> Result<Location, CsError> {
263 self.new_initial_timed_location(pg_id, &[])
264 }
265
266 pub fn new_initial_timed_location(
273 &mut self,
274 pg_id: PgId,
275 invariants: &[(Clock, TimeRange)],
276 ) -> Result<Location, CsError> {
277 let invariants = invariants
278 .iter()
279 .map(|(c, range)| {
280 if c.0 == pg_id {
281 Ok((c.1, *range))
282 } else {
283 Err(CsError::DifferentPgs(pg_id, c.0))
284 }
285 })
286 .collect::<Result<Vec<_>, CsError>>()?;
287 self.program_graphs
288 .get_mut(pg_id.0 as usize)
289 .ok_or(CsError::MissingPg(pg_id))
290 .and_then(|pg| {
291 pg.new_initial_timed_location(invariants)
292 .map(|loc| Location(pg_id, loc))
293 .map_err(|err| CsError::ProgramGraph(pg_id, err))
294 })
295 }
296
297 pub fn add_transition(
303 &mut self,
304 pg_id: PgId,
305 pre: Location,
306 action: Action,
307 post: Location,
308 guard: Option<CsGuard>,
309 ) -> Result<(), CsError> {
310 if action.0 != pg_id {
311 Err(CsError::ActionNotInPg(action, pg_id))
312 } else if pre.0 != pg_id {
313 Err(CsError::LocationNotInPg(pre, pg_id))
314 } else if post.0 != pg_id {
315 Err(CsError::LocationNotInPg(post, pg_id))
316 } else {
317 let guard = guard.map(|guard| {
319 guard.map(&|cs_var: Var| {
320 assert_eq!(cs_var.0, pg_id);
321 cs_var.1
322 })
323 });
324 self.program_graphs
325 .get_mut(pg_id.0 as usize)
326 .ok_or(CsError::MissingPg(pg_id))
327 .and_then(|pg| {
328 pg.add_transition(pre.1, action.1, post.1, guard)
329 .map_err(|err| CsError::ProgramGraph(pg_id, err))
330 })
331 }
332 }
333
334 pub fn add_timed_transition(
340 &mut self,
341 pg_id: PgId,
342 pre: Location,
343 action: Action,
344 post: Location,
345 guard: Option<CsGuard>,
346 constraints: &[(Clock, TimeRange)],
347 ) -> Result<(), CsError> {
348 if action.0 != pg_id {
349 Err(CsError::ActionNotInPg(action, pg_id))
350 } else if pre.0 != pg_id {
351 Err(CsError::LocationNotInPg(pre, pg_id))
352 } else if post.0 != pg_id {
353 Err(CsError::LocationNotInPg(post, pg_id))
354 } else {
355 let guard = guard.map(|guard| {
357 guard.map(&|cs_var: Var| {
358 assert_eq!(cs_var.0, pg_id);
359 cs_var.1
360 })
361 });
362 let constraints = constraints
363 .iter()
364 .map(|(c, range)| {
365 if c.0 == pg_id {
366 Ok((c.1, *range))
367 } else {
368 Err(CsError::DifferentPgs(pg_id, c.0))
369 }
370 })
371 .collect::<Result<Vec<_>, CsError>>()?;
372 self.program_graphs
373 .get_mut(pg_id.0 as usize)
374 .ok_or(CsError::MissingPg(pg_id))
375 .and_then(|pg| {
376 pg.add_timed_transition(pre.1, action.1, post.1, guard, constraints)
377 .map_err(|err| CsError::ProgramGraph(pg_id, err))
378 })
379 }
380 }
381
382 pub fn add_autonomous_transition(
388 &mut self,
389 pg_id: PgId,
390 pre: Location,
391 post: Location,
392 guard: Option<CsGuard>,
393 ) -> Result<(), CsError> {
394 if pre.0 != pg_id {
395 Err(CsError::LocationNotInPg(pre, pg_id))
396 } else if post.0 != pg_id {
397 Err(CsError::LocationNotInPg(post, pg_id))
398 } else {
399 let guard = guard.map(|guard| {
401 guard.map(&|cs_var: Var| {
402 assert_eq!(cs_var.0, pg_id);
403 cs_var.1
404 })
405 });
406 self.program_graphs
407 .get_mut(pg_id.0 as usize)
408 .ok_or(CsError::MissingPg(pg_id))
409 .and_then(|pg| {
410 pg.add_autonomous_transition(pre.1, post.1, guard)
411 .map_err(|err| CsError::ProgramGraph(pg_id, err))
412 })
413 }
414 }
415
416 pub fn add_autonomous_timed_transition(
422 &mut self,
423 pg_id: PgId,
424 pre: Location,
425 post: Location,
426 guard: Option<CsGuard>,
427 constraints: &[(Clock, TimeRange)],
428 ) -> Result<(), CsError> {
429 if pre.0 != pg_id {
430 Err(CsError::LocationNotInPg(pre, pg_id))
431 } else if post.0 != pg_id {
432 Err(CsError::LocationNotInPg(post, pg_id))
433 } else {
434 let guard = guard.map(|guard| {
436 guard.map(&|cs_var: Var| {
437 assert_eq!(cs_var.0, pg_id);
438 cs_var.1
439 })
440 });
441 let constraints = constraints
442 .iter()
443 .map(|(c, range)| {
444 if c.0 == pg_id {
445 Ok((c.1, *range))
446 } else {
447 Err(CsError::DifferentPgs(pg_id, c.0))
448 }
449 })
450 .collect::<Result<Vec<_>, CsError>>()?;
451 self.program_graphs
452 .get_mut(pg_id.0 as usize)
453 .ok_or(CsError::MissingPg(pg_id))
454 .and_then(|pg| {
455 pg.add_autonomous_timed_transition(pre.1, post.1, guard, constraints)
456 .map_err(|err| CsError::ProgramGraph(pg_id, err))
457 })
458 }
459 }
460
461 pub fn new_channel(&mut self, var_types: Vec<Type>, capacity: Option<usize>) -> Channel {
466 let channel = Channel(self.channels.len() as u16);
467 self.channels
468 .push((var_types, ChannelCapacity::Queue(capacity)));
469 channel
470 }
471
472 pub fn new_sink(&mut self, var_types: Vec<Type>) -> Channel {
474 let channel = Channel(self.channels.len() as u16);
475 self.channels.push((var_types, ChannelCapacity::Sink));
476 channel
477 }
478
479 pub fn new_send(
483 &mut self,
484 pg_id: PgId,
485 channel: Channel,
486 msgs: Vec<CsExpression>,
487 ) -> Result<Action, CsError> {
488 let channel_type = self
489 .channels
490 .get(channel.0 as usize)
491 .ok_or(CsError::MissingChannel(channel))?
492 .0
493 .to_owned();
494 let message_type = msgs.iter().map(|msg| msg.r#type()).collect::<Vec<_>>();
495 let msg = msgs
496 .into_iter()
497 .map(|msg| PgExpression::from((pg_id, msg)))
498 .collect::<Vec<_>>();
499 if channel_type != message_type {
500 Err(CsError::ProgramGraph(pg_id, PgError::TypeMismatch))
501 } else {
502 let action = self.program_graphs[pg_id.0 as usize]
503 .new_send(msg)
504 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
505 let action = Action(pg_id, action);
506 self.communications
507 .insert(action, Some((channel, Message::Send)));
508 Ok(action)
509 }
510 }
511
512 pub fn new_receive(
516 &mut self,
517 pg_id: PgId,
518 channel: Channel,
519 vars: Vec<Var>,
520 ) -> Result<Action, CsError> {
521 if let Some(var) = vars.iter().find(|var| pg_id != var.0) {
522 Err(CsError::VarNotInPg(*var, pg_id))
523 } else {
524 let channel_type = self
525 .channels
526 .get(channel.0 as usize)
527 .ok_or(CsError::MissingChannel(channel))?
528 .0
529 .to_owned();
530 let pg = self
531 .program_graphs
532 .get(pg_id.0 as usize)
533 .ok_or(CsError::MissingPg(pg_id))?;
534 let message_type = vars
535 .iter()
536 .map(|var| pg.var_type(var.1))
537 .collect::<Result<Vec<_>, _>>()
538 .map_err(|err| CsError::ProgramGraph(pg_id, err))?
539 .to_owned();
540 if channel_type != message_type {
541 Err(CsError::ProgramGraph(pg_id, PgError::TypeMismatch))
542 } else {
543 let action = self.program_graphs[pg_id.0 as usize]
544 .new_receive(vars.iter().map(|var| var.1).collect())
545 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
546 let action = Action(pg_id, action);
547 self.communications
548 .insert(action, Some((channel, Message::Receive)));
549 Ok(action)
550 }
551 }
552 }
553
554 pub fn new_probe_empty_queue(
558 &mut self,
559 pg_id: PgId,
560 channel: Channel,
561 ) -> Result<Action, CsError> {
562 let (_, cap) = self
563 .channels
564 .get(channel.0 as usize)
565 .ok_or(CsError::MissingChannel(channel))?;
566 if matches!(cap, ChannelCapacity::Queue(Some(0))) {
567 Err(CsError::ProbingHandshakeChannel(channel))
569 } else {
570 let action = self
571 .program_graphs
572 .get_mut(pg_id.0 as usize)
573 .ok_or(CsError::MissingPg(pg_id))?
574 .new_send(Vec::new())
576 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
577 let action = Action(pg_id, action);
578 self.communications
579 .insert(action, Some((channel, Message::ProbeEmptyQueue)));
580 Ok(action)
581 }
582 }
583
584 pub fn new_probe_full_queue(
588 &mut self,
589 pg_id: PgId,
590 channel: Channel,
591 ) -> Result<Action, CsError> {
592 let (_, cap) = self
593 .channels
594 .get(channel.0 as usize)
595 .ok_or(CsError::MissingChannel(channel))?;
596 if matches!(cap, ChannelCapacity::Queue(Some(0))) {
597 Err(CsError::ProbingHandshakeChannel(channel))
599 } else if matches!(cap, ChannelCapacity::Queue(None)) {
600 Err(CsError::ProbingInfiniteQueue(channel))
602 } else {
603 let action = self
604 .program_graphs
605 .get_mut(pg_id.0 as usize)
606 .ok_or(CsError::MissingPg(pg_id))?
607 .new_send(Vec::new())
609 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
610 let action = Action(pg_id, action);
611 self.communications
612 .insert(action, Some((channel, Message::ProbeFullQueue)));
613 Ok(action)
614 }
615 }
616
617 pub fn build(mut self) -> ChannelSystem {
619 let mut program_graphs: Vec<ProgramGraph> = self
620 .program_graphs
621 .into_iter()
622 .map(|builder| builder.build())
623 .collect();
624
625 program_graphs.shrink_to_fit();
626 self.channels.shrink_to_fit();
627 let communications_map = Vec::from_iter(self.communications);
628 let communications = Vec::from_iter(communications_map.iter().map(|&(_, comm)| comm));
629 let mut index = 0;
630 let mut communications_pg_idxs = Vec::<usize>::with_capacity(program_graphs.len() + 1);
631 communications_pg_idxs.push(index);
632 for pg_id in (0..program_graphs.len() as u16).map(PgId) {
633 index = communications_map[index..]
634 .iter()
635 .position(|(a, ..)| a.0.0 > pg_id.0)
636 .map_or(communications_map.len(), |pos| pos + index);
637 communications_pg_idxs.push(index);
638 }
639
640 assert_eq!(communications_pg_idxs.len(), program_graphs.len() + 1);
641
642 let cs = ChannelSystem {
643 channels: self.channels,
644 communications,
645 communications_pg_idxs,
646 program_graphs,
647 };
648
649 info!(
650 "create Channel System with: {} Program Graphs; {} channels; size {}",
651 cs.program_graphs.len(),
652 cs.channels.len(),
653 cs.get_size(),
654 );
655
656 cs
657 }
658}