Commit c683f697 authored by Maxime Perrotin's avatar Maxime Perrotin


parent fbd50933
(c) 2017-2018 European Space Agency / Maxime Perrotin
(c) 2017-2019 European Space Agency / Maxime Perrotin
This repository contains the components related to the model checker developed for TASTE.
......@@ -37,8 +37,61 @@ During the simulation, after each step the properties are evaluated and a pop-up
After installing asn1-iterators, make sure you export
`asn1-iterators` allows to iterate over the values of ASN.1 data types, using the standard Ada syntax.
This is how it works: for example given a type `MySeq` defined in an ASN.1 grammar like this:
MySeq ::= SEQUENCE {
a MyInteger, -- INTEGER (1..4)
b MyEnum -- ENUMERATED { hello, world, how-are-you }
If you run the following script:
$ taste-asn1-iterators DataView.asn
You can then write an Ada application that contains:
with ASN1_Ada_Iterators.Iterators; -- This package was generated
use ASN1_Ada_Iterators.Iterators;
-- Declare an iterator
Seq : MySeq_Pkg.Instance;
-- And in the core of the application, you can iterate like this:
for Each of Seq loop
Put (Image (Each) & " "); -- Each is an instance of the ASN.1 type "MySeq"
end loop;
When you execute your program, you will see:
{a 1, b hello} {a 1, b world} {a 1, b how_are_you} {a 2, b hello} {a 2, b world}
{a 2, b how_are_you} {a 3, b hello} {a 3, b world} {a 3, b how_are_you} {a 4, b hello}
{a 4, b world} {a 4, b how_are_you}
To build your application using gprbuild, after installing asn1-iterators, make sure you export
And in your gpr project file, put:
with "asn1_iterators";
There is a complete test case that you can build using `make test` in the asn1-iterators folder. Check the .gpr and the source code (`test_generic.adb`) to get an overview of the possiblities.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment