[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Automata connection

Dear Sirs,

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 
evaluated earlier.

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 
VS records
to input record of particular automaton.

In the real world I solve this thru references to automata, but I don't 
know, how
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.

Best regards

Robert Kolcava