amutake/actario

Verification Framework for Actor Systems on Coq

actario's Issues

logo

Supervisor

To introduce supervisor, I have to:

• Survey supervisor usage and supervisor hierarchy of Erlang and Akka
• Formalize supervisors (maybe using hierarchical names)
• Think out proof methods in case of using supervisors

transition path

Move to psg-titech

Fairness

define as Axiom or Definition using transition path (#7).

ssreflect based

I want to use MathComp.finset

Unreliable semantics

like Verdi

Coq8.5 and Ssreflect1.6

Remove global message queue

If global message queue is removed, the definition of config becomes just list actor.
This is required for implementing sub-configuration (#4).

Change `actor` definition to Record

and remove Getter module.

Example using fairness

more information in transition label (trans_type)

and rename trans_type -> label

Inductive label :=
| Receive dest source content (* `dest` receives a message `content` from `source` *)
| Send source dest content    (* `source` sends a message `content` to `dest` *)
| New parent child            (* `parent` creates an actor named `child` *)
| Self myname                 (* `myname` gets own name *)

This is required for fairness (enabled definition). #8

Do something about Japanese comments

Current comments are awful...

move to docs/ja?

Sub-configuration and message delivery from/to external actor

Split Send transition to 2 cases (#2 is required).

1. if the target is in the configuration
2. if the target is not in the configuration