Correctness

Correctness, in the context of the GMT Actors Model, refers to the verification process that checks for error in the code written by users of the gmt-dos-actor API. The code is checked for mistakes both at compiled-time and at runtime. This formal process makes developping an integrated model with gmt-dos-actor very safe as it ensures that the likehood of having written a "correct" model is very high.

A "correct' model is a model build with Rust code that complies with the following:

1. a pair of input and output must have the same UID,
2. a pair of input and output must have the same sampling rate: NI=NO,
3. an actor with an input sampling rate NI=0 must have no input,
4. an actor with an input sampling rate NI>0 must have at least one input,
5. an actor with an output sampling rate NO=0 must have no output,
6. an actor with an output sampling rate NO>0 must have at least one output,
7. in a model, taking into account all actors, there must be as many inputs as outputs,
8. in a model, taking into account all actors, the sum of inputs hashes must be equal to the sum of the outputs hashes.

If the code doesn't comply with any of the aboves, either it won't compile sucessfully or it will panic before the model is run.

For rapid troubleshooting it is important to be able to associate error messages with the corresponding compliance clause. In the following, we give examples of faulty code, with the generated error messsage, for some of the compliance clauses:

• a pair of input and output must have the same UID

    let mut timer: Initiator<_> = Timer::new(3).into();
    let mut signals: Actor<_> = Signals::new(1, 3).into();
    timer.add_output().build::<In>();

    let mut timer: Initiator<_> = Timer::new(3).into();
    let mut logging = Logging::<f64>::new(2).into_arcx();
    let mut logger = Terminator::<_>::new(logging.clone());
    timer.add_output().build::<Tick>().into_input(&mut logger);

• a pair of input and output must have the same sampling rate: NI=NO

    let mut timer: Initiator<_> = Timer::new(3).into();
    let mut signals: Actor<_, 2> = Signals::new(1, 3).into();
    timer
        .add_output()
        .build::<Tick>()
        .into_input(&mut signals)
        .unwrap();

• an actor with an input sampling rate NI>0 must have at least one input

            let mut timer: Actor<Timer, 1> = Timer::new(3).into();
            let mut signals: Actor<Signals, 1> = Signals::new(1, 3).into();
            timer
                .add_output()
                .build::<Tick>()
                .into_input(&mut signals)?;
            model!(timer, signals).check()?;

• an actor with an output sampling rate NO>0 must have at least one output,

            let mut timer: Initiator<_> = Timer::new(3).into();
            let mut signals: Actor<_> = Signals::new(1, 3).into();
            timer
                .add_output()
                .build::<Tick>()
                .into_input(&mut signals)?;
            let logging = Logging::<f64>::new(1).into_arcx();
            let mut logger = Actor::<_>::new(logging.clone());
            #[derive(UID)]
            enum Sig {}
            signals
                .add_output()
                .build::<Sig>()
                .into_input(&mut logger)?;
            model!(timer, signals, logger).check()?;

• in a model, taking into account all actors, there must be as many inputs as outputs,

            let mut timer: Initiator<_> = Timer::new(3).into();
            let mut signals: Actor<_> = Signals::new(1, 3).into();
            timer
                .add_output()
                .build::<Tick>()
                .into_input(&mut signals)?;
            let logging = Logging::<f64>::new(1).into_arcx();
            let mut logger = Terminator::<_>::new(logging.clone());
            #[derive(UID)]
            enum Sig {}
            signals
                .add_output()
                .build::<Sig>()
                .into_input(&mut logger)?;
            model!(timer, signals).check()?;