========================================================================
    CIRCUS REFINE 
========================================================================

#Font:

The Circus Refine also requires an installation of CZT font. 

Installing CZTSans font in Windows:

   1. Choose Start > Settings > Control Panel

      Note: In Windows XP, choose Start > Control Panel
       
   2. Double-click the Fonts folder.
       
   3. Choose File > Install New Font.
       
   4. Locate the CZTSans font in CircusRefine/font.
             
   5. Select the fonts to install. 
       
   6. To copy the fonts to the Fonts folder, make sure the Copy fonts to the Fonts folder check box is selected.
       
   7. Click OK to install the fonts.

#Images:

Theses files are also needed in Circus Refine interface. 

#veriT:

Theses files are also needed in Circus Refine Proof Obligation Discharge system. 

#novoSty:

Theses files are also needed in Circus Refine Document Generation. 

#######

#Start Development
In order to start the refinement of a specification, the user must open the specification in the .tex format within the tool. 
For that, the user must select "Development -> New" from the menu. 


/////////////////////////////////////////////////////////////////////////////

##Case Studies 

####PID

The strategy of this case study is to verify SPARK Ada programs with respect
to Simulink diagrams using Circus. This verification is based on calculating a
Circus model for the diagram and calculating a Circus model for the SPARK
Ada program, and proving that the former is refned by the latter.

In order to execute the PID the user must 

1. Open the PID.tex which is in Case Studies -> PID

2. Once the specification is open, it is necessary select all the specification. This selection is realised on the lines of the development window; hold the CTRL key and click on the first and last line of the term in order to select multiple lines. 

3. Once you have selected a term, using the right button, click on the selected term to visualise the pop-up menu. 

4. Go to "Apply Tactic" on the menu 

5. Select the NB tactic. 

6. After the NB application, select the result 

7. Using the pop-up menu go to "Apply Tactic" 

8. Select the BJ tactic.

##### JCircus

The user of CRefine can also generate Java code that implements the
specification in Circus, using JCircus. For that, the user must:

1. Run CRefine

2. Open a Specification written in LaTeX Circus (using the "new"
button, under the "Refinement" label)

3. Having opened the specification, the user will see three panels:
"Refinement", "Code" and "Proof Obligation". Positioning the mouse on
the Specification inside the "Code" panel, the user must right-click
on its mouse. After that, a pop-up menu will appear with button
"JCircus". Positioning the mouse in "JCircus", then another button
appears, called "Translate 2 Java".

4. Choose the folder in which the user wishes to store the generated code.

5. Click "Ok
