[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Automata connection
I need to compose some automata.
Each automaton is specified in its own theory.
It has input record I,
variable and state record VS,
transition function [I, VS -> VS].
I can proof some invariants over this particular automata.
But I need connect them into larger machine and for this to proof
The connection (or composition) is strict sequential, no events.
One automaton can "read" input data only from automata, which was
The machine transition function is then composition of transition functions
of all automata and the machine variable and state record is union of
and state records of all automata.
But for "connection" of automata I need the "input map function" to map
to input record of particular automaton.
In the real world I solve this thru references to automata, but I don't
to do this in PVS.
And the second problem, in this specification of "whole machine" isn't
known number of
(e.g.) input automata [1..N], that means, the input for output automaton
is an array
of outputs of all input automata.
In the real world I solve this thru array of references to input automata.
I need to proof some invariants for uninterpreted N: nat.
Can you help me? Thanks.