Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
TASTE
Ocarina
Commits
306dcf5b
Commit
306dcf5b
authored
Jun 01, 2018
by
yoogx
Browse files
* Correct reference output
parent
2dae8d60
Changes
8
Expand all
Hide whitespace changes
Inline
Side-by-side
tests/real-annexes-execution/test_real_exec_02.aadl.out
View file @
306dcf5b
...
...
@@ -151,22 +151,22 @@ Evaluating theorem set_declaration_is_passing_through
* Iterate for variable: rma.erc32_node_a_task_1
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :40
2
4 end to end flow spec
anonymous end to end flow :40
1
4 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_2
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :40
2
4 end to end flow spec
anonymous end to end flow :40
1
4 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_12
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :40
2
5 end to end flow spec
anonymous end to end flow :40
1
5 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_22
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :40
2
5 end to end flow spec
anonymous end to end flow :40
1
5 end to end flow spec
=> Result: TRUE
theorem set_declaration_is_passing_through is: TRUE
...
...
tests/real-annexes-parsing/test_real_parse_01.aadl.out
View file @
306dcf5b
...
...
@@ -78,7 +78,7 @@ property set Deployment is
Protocol
:
Deployment
::
Protocol_Type
applies
to
(
system
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_ORK
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
ARM_CORTEX
,
ARM_DSLINUX
,
ARM_N770
,
GUMSTIX_RTEMS
,
NDS_RTEMS
,
X86_RTEMS
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Execution_Platform
:
Deployment
::
Allowed_Execution_Platform
applies
to
(
all
);
...
...
@@ -685,10 +685,10 @@ system)
applies
to
(
system
);
dataview
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
dataviewpath
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
Encoding_type
:
type
enumeration
(
native
,
uper
,
acn
);
...
...
tests/real-annexes-parsing/test_real_parse_02.aadl.out
View file @
306dcf5b
...
...
@@ -78,7 +78,7 @@ property set Deployment is
Protocol
:
Deployment
::
Protocol_Type
applies
to
(
system
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_ORK
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
ARM_CORTEX
,
ARM_DSLINUX
,
ARM_N770
,
GUMSTIX_RTEMS
,
NDS_RTEMS
,
X86_RTEMS
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Execution_Platform
:
Deployment
::
Allowed_Execution_Platform
applies
to
(
all
);
...
...
@@ -685,10 +685,10 @@ system)
applies
to
(
system
);
dataview
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
dataviewpath
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
Encoding_type
:
type
enumeration
(
native
,
uper
,
acn
);
...
...
tests/real-annexes-parsing/test_real_parse_03.aadl.out
View file @
306dcf5b
...
...
@@ -78,7 +78,7 @@ property set Deployment is
Protocol
:
Deployment
::
Protocol_Type
applies
to
(
system
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_ORK
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
ARM_CORTEX
,
ARM_DSLINUX
,
ARM_N770
,
GUMSTIX_RTEMS
,
NDS_RTEMS
,
X86_RTEMS
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Execution_Platform
:
Deployment
::
Allowed_Execution_Platform
applies
to
(
all
);
...
...
@@ -685,10 +685,10 @@ system)
applies
to
(
system
);
dataview
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
dataviewpath
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
Encoding_type
:
type
enumeration
(
native
,
uper
,
acn
);
...
...
tests/real-annexes-parsing/test_real_parse_04.aadl.out
View file @
306dcf5b
...
...
@@ -78,7 +78,7 @@ property set Deployment is
Protocol
:
Deployment
::
Protocol_Type
applies
to
(
system
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_ORK
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
ARM_CORTEX
,
ARM_DSLINUX
,
ARM_N770
,
GUMSTIX_RTEMS
,
NDS_RTEMS
,
X86_RTEMS
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Execution_Platform
:
Deployment
::
Allowed_Execution_Platform
applies
to
(
all
);
...
...
@@ -685,10 +685,10 @@ system)
applies
to
(
system
);
dataview
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
dataviewpath
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
Encoding_type
:
type
enumeration
(
native
,
uper
,
acn
);
...
...
tests/real-annexes-parsing/test_real_parse_05.aadl.out
View file @
306dcf5b
...
...
@@ -78,7 +78,7 @@ property set Deployment is
Protocol
:
Deployment
::
Protocol_Type
applies
to
(
system
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_ORK
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
ARM_CORTEX
,
ARM_DSLINUX
,
ARM_N770
,
GUMSTIX_RTEMS
,
NDS_RTEMS
,
X86_RTEMS
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Execution_Platform
:
Deployment
::
Allowed_Execution_Platform
applies
to
(
all
);
...
...
@@ -685,10 +685,10 @@ system)
applies
to
(
system
);
dataview
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
dataviewpath
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
Encoding_type
:
type
enumeration
(
native
,
uper
,
acn
);
...
...
tests/test042/test.aadl.out
View file @
306dcf5b
...
...
@@ -74,7 +74,7 @@ property set Deployment is
Protocol
:
Deployment
::
Protocol_Type
applies
to
(
system
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_ORK
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
ARM_CORTEX
,
ARM_DSLINUX
,
ARM_N770
,
GUMSTIX_RTEMS
,
NDS_RTEMS
,
X86_RTEMS
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Allowed_Execution_Platform
:
type
enumeration
(
Native
,
Native_Compcert
,
bench
,
GNAT_Runtime
,
LEON_RTEMS
,
LEON_RTEMS_POSIX
,
LEON3_SCOC3
,
LEON3_XTRATUM
,
LEON3_XM3
,
LEON_GNAT
,
LINUX32
,
LINUX32_XENOMAI_NATIVE
,
LINUX32_XENOMAI_POSIX
,
LINUX64
,
ERC32_ORK
,
X86_RTEMS_POSIX
,
X86_LINUXTASTE
,
MARTE_OS
,
WIN32
,
VXWORKS
,
FREERTOS
);
Execution_Platform
:
Deployment
::
Allowed_Execution_Platform
applies
to
(
all
);
...
...
@@ -681,10 +681,10 @@ system)
applies
to
(
system
);
dataview
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
dataviewpath
:
list
of
aadlstring
applies
to
(
package
,
system
);
applies
to
(
package
);
Encoding_type
:
type
enumeration
(
native
,
uper
,
acn
);
...
...
tests/test_tree_p2/test.aadl.out
View file @
306dcf5b
This diff is collapsed.
Click to expand it.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment