diff --git a/doc/ocarina-config.1 b/doc/ocarina-config.1 index 44ab42e40b13a0db48a562d35642425ffd296707..b26019fd567338569dcc0b673800875936dda5e0 100644 --- a/doc/ocarina-config.1 +++ b/doc/ocarina-config.1 @@ -1,5 +1,5 @@ .\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.10. -.TH OCARINA "1" "avril 2013" "Ocarina 2.0w" "User Commands" +.TH OCARINA "1" "mars 2016" "Ocarina 2.0w" "User Commands" .SH NAME Ocarina \- manual page for Ocarina 2.0w .SH SYNOPSIS diff --git a/doc/ocarina-config.html b/doc/ocarina-config.html index 05601b05abdeaa25a0be470d4f5a9169e45301a1..071abab937cabd8bcd0d6b84a959a9b06ff63830 100644 --- a/doc/ocarina-config.html +++ b/doc/ocarina-config.html @@ -1,5 +1,5 @@ - + diff --git a/doc/ocarina.1 b/doc/ocarina.1 index 6399afe9624dc9b92c5df8d98e4c7dc52ad9d3c8..97adcee0eb8bdaa64ce9715d41560946bfe17b40 100644 --- a/doc/ocarina.1 +++ b/doc/ocarina.1 @@ -1 +1,113 @@ +.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.10. +.TH OCARINA "1" "mars 2016" "Ocarina 2.0w (Working Copy from rb472173)" "User Commands" +.SH NAME +Ocarina \- manual page for Ocarina 2.0w (Working Copy from rb472173) +.SH SYNOPSIS +.B ocarina +[\fIswitches\fR] \fI\fR +.SH DESCRIPTION +.TP +\fB\-h\fR, \fB\-\-help\fR +Display help and exit +.TP +\fB\-\-version\fR +Display version and exit +.TP +\fB\-v\fR, \fB\-\-verbose\fR +Output extra verbose information +.TP +\fB\-q\fR +Quiet mode (default) +.TP +\fB\-d\fR +Debug mode +.TP +\fB\-s\fR +Output default search directory, then exit +.TP +\fB\-aadlv[ARG]\fR +AADL version, ARG = 1 for AADL 1.0, 2 for AADL 2.x +.TP +\fB\-f\fR +Parse predefined non\-standard property sets +.HP +\fB\-disable\-annexes\fR=\fIARG\fR Deactivate annex ARG +.TP +\fB\-r\fR ARG +Use ARG as root system +.TP +\fB\-o\fR ARG +Specify output file/directory +.TP +\fB\-y\fR +Automatically load AADL files +.TP +\fB\-I\fR ARG +Add ARG to the directory search list +.TP +\fB\-p\fR +Parse and instantiate the model +.TP +\fB\-i\fR +Instantiate the model +.TP +\fB\-x\fR +Parse AADL file as an AADL scenario file +.TP +\fB\-g\fR ARG +Generate code using Ocarina backend 'ARG' +.TP +\fB\-\-list\-backends\fR +List available backends +.TP +\fB\-b\fR +Compile generated code +.TP +\fB\-z\fR +Clean code generated +.TP +\fB\-k\fR ARG +Set POK flavor (arinc653/deos/pok/vxworks) +.TP +\fB\-t\fR +Run Ocarina in terminal interactive mode +.TP +\fB\-real_theorem\fR ARG +Name of the main theorem to evaluate +.TP +\fB\-real_lib\fR ARG +Add external library of REAL theorems +.TP +\fB\-real_continue_eval\fR +Continue evaluation of REAL theorems after first failure (REAL backend) +.TP +\fB\-boundt_process\fR ARG +Generate .tpo file for process ARG (Bound\-T backend) +.TP +\fB\-ec\fR +Compute coverage metrics +.TP +\fB\-er\fR +Execute system +.TP +\fB\-asn1\fR +Generate ASN1 deployment file (PolyORB\-HI\-C only) +.TP +\fB\-perf\fR +Enable profiling with gprof (PolyORB\-HI\-C only) +.SH COPYRIGHT +Copyright \(co 2003\-2009 Telecom ParisTech, 2010\-2016 ESA & ISAE +Build date: +.SH "SEE ALSO" +The full documentation for +.B Ocarina +is maintained as a Texinfo manual. If the +.B info +and +.B Ocarina +programs are properly installed at your site, the command +.IP +.B info Ocarina +.PP +should give you access to the complete manual. .HEAD "" diff --git a/doc/ocarina_man.html b/doc/ocarina_man.html index 515194851233e3321002bd7311319ac9f91c27c3..56ca6956422a7d520ed7d71f704e8ffa117c6582 100644 --- a/doc/ocarina_man.html +++ b/doc/ocarina_man.html @@ -1,5 +1,5 @@ - + @@ -21,7 +21,9 @@

OCARINA

NAME
+SYNOPSIS
DESCRIPTION
+COPYRIGHT
SEE ALSO

@@ -32,23 +34,36 @@

Ocarina − -manual page for Ocarina 2.0w (Working Copy from )

+manual page for Ocarina 2.0w (Working Copy from +rb472173)

+ + +

SYNOPSIS

+ + +

ocarina +[switches] <aadl_files>

DESCRIPTION

-

Usage:

+

−h, +−−help

+ +

Display help and exit

+ + +

−−version

-

ocarina [options] files OR -ocarina −help

+

Display version and exit

-

files are a non -null sequence of AADL files

+

−v, +−−verbose

-

General purpose -options:

+

Output extra verbose +information

@@ -58,13 +73,13 @@ options:

-

−V

+

−q

+

Quiet mode +(default)

@@ -73,314 +88,304 @@ version, then exit

-

−s

+

−d

+

Debug mode

-
-

Output Ocarina -version, then exit

-

Output Ocarina -search directory, then exit

- -

Scenario file -options:

- - +

−s

- - + +
-

−b

+ -

Generate and build -code from the AADL model

+

Output default +search directory, then exit

+ +

−aadlv[ARG]

+ +

AADL version, ARG = 1 for AADL +1.0, 2 for AADL 2.x

+ + +

−f

+

Parse predefined +non−standard property sets

-

−z

-

Clean code -generated from the AADL model

-

−ec -Execute the generated application code and

- -

retrieve -coverage information

- - -

−er -Execute the generated application code and

- -

verify that -there is no regression

+

−disable−annexes=ARG +Deactivate annex ARG

- + + - - - + - - - + + - + -
+ +

−r +ARG

-

−p

- -

Only parse and -instantiate the application model

+

Use ARG as root +system

+ - -

−c

+

−o +ARG

-

Only perform -schedulability analysis

+

Specify output +file/directory

- -

Advanced user -options:

- - - - - + + +

Automatically load +AADL files

+ - - - + + +

Add ARG to the +directory search list

+ - - - + + +

Parse and +instantiate the model

+ - - - + + +

Instantiate the +model

+ - - - + + - - - + + - - - + +
+ -

−d

+

−y

-

Debug mode for -developpers

+
- + -

−q

+

−I +ARG

-

Quiet mode -(default)

+
+ -

−t

+

−p

-

[script] Run -Ocarina in terminal interactive mode. If a script is given, -interpret it then exit.

+
+ -

−v

+

−i

-

Verbose mode for -users

+
+

−x

+

Parse AADL file as an AADL scenario file

+
- - + -

−y

+

−g +ARG

-

Automatically load -AADL files on demand

+

Generate code using +Ocarina backend ’ARG’

+
-

−f

- - +

−−list−backends

+

List available backends

-

Parse predefined -non standard property sets

+ - - - + + +

Compile generated +code

+ - - - + + +

Clean code +generated

+ - - - + + +

Set POK flavor +(arinc653/deos/pok/vxworks)

+ - - - + + +

Run Ocarina in +terminal interactive mode

+
+ -

−i

+

−b

-

Instantiate the -AADL model

+
+ -

−r

+

−z

-

<name> The -name of the instance tree root

+
- + -

−o

+

−k +ARG

-

Specify output -file

+
+ -

−I

+

−t

-

Specify the -inclusion paths

+
-

−aadlv1

+

−real_theorem +ARG

-

Use AADL v1 standard -(default)

+

Name of the main theorem to +evaluate

-

−aadlv2

+

−real_lib ARG

-

Use AADL v2 standard

+

Add external library of REAL +theorems

-

−real_lib -Add a REAL file to be used as a theorem library by REAL -annexes

+

−real_continue_eval

+

Continue evaluation of REAL +theorems after first failure (REAL backend)

-

−real_theorem -<theorem> Evaluate only theorem

+

−boundt_process +ARG

- -

−real_continue_eval -Continue evaluation in case of failures

+

Generate .tpo file for process +ARG (Bound−T backend)

- - - + + -
- + -

−g

+

−ec

-

Generate code from -the AADL instance tree Registered backends:

- -

arinc653_conf -petri_nets boundt mast polyorb_hi_ada polyorb_hi_c -polyorb_hi_rtsj pok_c xtratum_configuration stats -subprograms real_theorem carts asn1_deployment cheddar -connection_matrix function_matrix aadl_xml aadl aadl_min -aadl_annex behavior_specification real_specification

- +

Compute coverage +metrics

+ +

−er

+

Execute system

@@ -398,62 +403,30 @@ with gprof (PolyORB−HI−C only)

deployment file (PolyORB−HI−C only)

-
+
-

−perf

-

Enable profiling -with gprof (PolyORB−HI−C only)

- -

−arinc653

- -

Generate code for ARINC653 API -(POK backend only)

- - - - - + + - - - +

Enable profiling +with gprof (PolyORB−HI−C only)

- - -
+ -

−b

+

−perf

-

Generate and build -code from the AADL model

-
- - - -

−z

- - -

Clean code -generated from the AADL model

+ +

COPYRIGHT

-

−disable−annexes={annexes}

- -

Desactive one or all -annexes

- -

Annexes :

- -

all behavior -real

-

Build date: -Saturday 20 April 2013, 16:54:47 Copyright © -2003−2009 Telecom ParisTech, 2010−2013 ESA & -ISAE

+

Copyright +© 2003−2009 Telecom ParisTech, 2010−2016 +ESA & ISAE Build date:

SEE ALSO