========================================================================
    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. 

#Examples:

This Folder contains some parseable files according CZT parser of 6116 revision 
(09/24/2007 - 18:45).  

/////////////////////////////////////////////////////////////////////////////
Other notes:

-> The output file .tex generated by the CircusRefine's Print feature requires 
circus.sty, zed.sty, csp.sty.  
-> The circus.sty is still in devolpment by CZT.


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

#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 open the PID.tex which is in Case Studies -> PID
Afterwards, 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. 
Once you have selected a term, using the right button, click on the selected term to visualise the pop-up menu.
Go to "Apply Tactic" on the menu and select the NB tactic.
After the NB application, select the result and using the pop-up menu
go to "Apply Tactic" and select the BJ tactic.
