a slight problem need some help. Simulation Control System

a slight problem need some help. Simulation Control System

[Mr.Spark]

I had a problem when I run examiner to check if the body package is
working fine but the problem it gives me:

Specification Part:

with Sensor, Pump;

--# inherit Sensor, Pump;

package Tank

--# own Tank_Level;
--# initializes Tank_Level;

is
   procedure Control;

   --# global out Tank_Level;
   --#        in Sensor.Level;
   --#        in out Pump.Pump_Open;
   --# derives Tank_Level from Sensor.Level &
   --#         Pump.Pump_Open from Sensor.Level, Pump.Pump_Open;


end Tank;

Body Package Is :

with Sensor, Pump;

package body Tank

is

   Empty: constant Sensor.Level_Type := 10;
   Full: constant Sensor.Level_Type := 60;

   -- this procedure controls the operation of pumps when they should
be opened
   -- or closed for the safety of the system. The pump will be closed
if the
   -- Water Level Tank is <= 10 and it will be Opened if the Water
Level
   -- in Tank >= 60.

   procedure Control
   is
      Tank_Level: Sensor.Level_Type;
   begin

      Tank_Level:= Sensor.Get_Level;
      if Tank_Level <= Empty then
         Pump.Close;
      elsif Tank_Level >= Full then
         Pump.Open;
      end if;
   end Control;

end Tank;


The errors that it shows are :


1.Semantic Error : Ilegal redeclaration of identifier Tank_Level;
2.Semantic Error : The Identifier is either undeclared or not visible
at his point
3.Semantic Error : The Identifier is either undeclared or not visible
at his point1.
4.Semantic Error : The Identifier is either undeclared or not visible
at his point
5.Semantic Error : The own variable Tank_Level does not have a
definition

If you could give me a hint how to solve this problem it would be
great.

Re: a slight problem need some help. Simulation Control System

[Phil Thornley]

On 13 Nov, 16:09, "Mr.Spark" <malma...@gmail.com> wrote:
> I had a problem when I run examiner to check if the body package is
> working fine but the problem it gives me:
>
> Specification Part:
>
> with Sensor, Pump;
>
> --# inherit Sensor, Pump;
>
> package Tank
>
> --# own Tank_Level;
> --# initializes Tank_Level;
>
> is
>    procedure Control;
>
>    --# global out Tank_Level;
>    --#        in Sensor.Level;
>    --#        in out Pump.Pump_Open;
>    --# derives Tank_Level from Sensor.Level &
>    --#         Pump.Pump_Open from Sensor.Level, Pump.Pump_Open;
>
> end Tank;
>
> Body Package Is :
>
> with Sensor, Pump;
>
> package body Tank
>
> is
>
>    Empty: constant Sensor.Level_Type := 10;
>    Full: constant Sensor.Level_Type := 60;
>
>    -- this procedure controls the operation of pumps when they should
> be opened
>    -- or closed for the safety of the system. The pump will be closed
> if the
>    -- Water Level Tank is <= 10 and it will be Opened if the Water
> Level
>    -- in Tank >= 60.
>
>    procedure Control
>    is
>       Tank_Level: Sensor.Level_Type;
>    begin
>
>       Tank_Level:= Sensor.Get_Level;
>       if Tank_Level <= Empty then
>          Pump.Close;
>       elsif Tank_Level >= Full then
>          Pump.Open;
>       end if;
>    end Control;
>
> end Tank;
>
> The errors that it shows are :
>
> 1.Semantic Error : Ilegal redeclaration of identifier Tank_Level;
> 2.Semantic Error : The Identifier is either undeclared or not visible
> at his point
> 3.Semantic Error : The Identifier is either undeclared or not visible
> at his point1.
> 4.Semantic Error : The Identifier is either undeclared or not visible
> at his point
> 5.Semantic Error : The own variable Tank_Level does not have a
> definition
>
> If you could give me a hint how to solve this problem it would be
> great.

The main problem is that the 'own' annotation on the spec states that
the variable Tank_Level will be declared in the package body - as
permanent data.  But the code only creates it as local data within the
Control procedure.  So Tank_Level is created as uninitialised data
each time that the Control procedure is invoked.

If you move the declaration of Tank_Level to the package body then you
will remove some of the errors.  Alterntively if the data should be
local to the Control procedure then it should not be declared as 'own'
data in the package specification.

For more accurate error diagnosis, include at least the specs of all
the other referenced packages (ie Sensor and Pump in this case) so
that we can do a complete SPARK run.

Cheers,

Phil

Re: a slight problem need some help. Simulation Control System

[Mr.Spark]

On Nov 13, 4:54 pm, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:
> On 13 Nov, 16:09, "Mr.Spark" <malma...@gmail.com> wrote:
>
>
>
> > I had a problem when I run examiner to check if the body package is
> > working fine but the problem it gives me:
>
> > Specification Part:
>
> > with Sensor, Pump;
>
> > --# inherit Sensor, Pump;
>
> > package Tank
>
> > --# own Tank_Level;
> > --# initializes Tank_Level;
>
> > is
> >    procedure Control;
>
> >    --# global out Tank_Level;
> >    --#        in Sensor.Level;
> >    --#        in out Pump.Pump_Open;
> >    --# derives Tank_Level from Sensor.Level &
> >    --#         Pump.Pump_Open from Sensor.Level, Pump.Pump_Open;
>
> > end Tank;
>
> > Body Package Is :
>
> > with Sensor, Pump;
>
> > package body Tank
>
> > is
>
> >    Empty: constant Sensor.Level_Type := 10;
> >    Full: constant Sensor.Level_Type := 60;
>
> >    -- this procedure controls the operation of pumps when they should
> > be opened
> >    -- or closed for the safety of the system. The pump will be closed
> > if the
> >    -- Water Level Tank is <= 10 and it will be Opened if the Water
> > Level
> >    -- in Tank >= 60.
>
> >    procedure Control
> >    is
> >       Tank_Level: Sensor.Level_Type;
> >    begin
>
> >       Tank_Level:= Sensor.Get_Level;
> >       if Tank_Level <= Empty then
> >          Pump.Close;
> >       elsif Tank_Level >= Full then
> >          Pump.Open;
> >       end if;
> >    end Control;
>
> > end Tank;
>
> > The errors that it shows are :
>
> > 1.Semantic Error : Ilegal redeclaration of identifier Tank_Level;
> > 2.Semantic Error : The Identifier is either undeclared or not visible
> > at his point
> > 3.Semantic Error : The Identifier is either undeclared or not visible
> > at his point1.
> > 4.Semantic Error : The Identifier is either undeclared or not visible
> > at his point
> > 5.Semantic Error : The own variable Tank_Level does not have a
> > definition
>
> > If you could give me a hint how to solve this problem it would be
> > great.
>
> The main problem is that the 'own' annotation on the spec states that
> the variable Tank_Level will be declared in the package body - as
> permanent data.  But the code only creates it as local data within the
> Control procedure.  So Tank_Level is created as uninitialised data
> each time that the Control procedure is invoked.
>
> If you move the declaration of Tank_Level to the package body then you
> will remove some of the errors.  Alterntively if the data should be
> local to the Control procedure then it should not be declared as 'own'
> data in the package specification.
>
> For more accurate error diagnosis, include at least the specs of all
> the other referenced packages (ie Sensor and Pump in this case) so
> that we can do a complete SPARK run.
>
> Cheers,
>
> Phil

Hi Phil,

Thanks a lot for replying in a short time. I Appreciate your help.
that solved the problem. :)