Skip to content

GitLab

Commit 3a7bd047 authored by Daniel Ratiu's avatar Daniel Ratiu
Browse files

the assumptions are used when the verification is performed 

refs 862
parent a6c664e7
Hide whitespace changes
Inline Side-by-side
org.fortiss.af3.rcp.application/trunk/html/model_checking_with_af3.html
View file @ 3a7bd047
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
@author becker @author becker
@author $Author$ @author $Author$
@version $Rev$ @version $Rev$
@ConQAT.Rating GREEN Hash: 220A678AB78B2A4B1DB7BC3B762A1C90 @ConQAT.Rating GREEN Hash: FA131DC4463BEECA646C85A828A1B991
--> -->
<html> <html>
...@@ -98,9 +98,12 @@ corresponding state automaton will be opened and the unreachable state will be h ...@@ -98,9 +98,12 @@ corresponding state automaton will be opened and the unreachable state will be h
<li> <b>Step 4.2</b> - Select a verification context from the 'Verification Context' combo <li> <b>Step 4.2</b> - Select a verification context from the 'Verification Context' combo
(the verification context indicates the part of the model that will be used for verification; (the verification context indicates the part of the model that will be used for verification;
selecting a context bigger than the component to be checked helps to restrict the set of input values for the checked component selecting a context bigger than the component to be checked helps to restrict the set of input values for the checked component
because the model checker will not consider all input values but only those possible according to the selected context). because the model checker will not consider all input values but only those possible according to the selected context).
All assumptions attached to the component selected as verification context (for more information about attaching assumptions
to a component see the help page for <a href="tl_specification.html">Contracts Specification View</a>)
are taken into account when the verification is performed.
<li> <b>Step 4.2</b> - Write the condition to be checked in one of the fields from below and by using the same syntax <li> <b>Step 4.2</b> - Write the condition to be checked in one of the fields from below and by using the same syntax
as for specifying guards for transitions. In case of failure a counterexample will be displayed. as for specifying guards for transitions. In case of failure a counterexample will be displayed.
<br> <br>
<br> <br>
<br> <br>
......
org.fortiss.af3.rcp.application/trunk/html/tl_specification.html
View file @ 3a7bd047
...@@ -6,7 +6,7 @@ Contracts-based Specification for Components. ...@@ -6,7 +6,7 @@ Contracts-based Specification for Components.
@author becker @author becker
@author $Author: becker $ @author $Author: becker $
@version $Rev: 3250 $ @version $Rev: 3250 $
@ConQAT.Rating GREEN Hash: 47CB773694313EF05AEA0E73F5B767E3 @ConQAT.Rating GREEN Hash: F45C3DE9A654E93163AC0C9149FA9CB6
--> -->
<html> <html>
...@@ -57,7 +57,8 @@ As we can see in the lower part of the figure, this view has five tabs: the firs ...@@ -57,7 +57,8 @@ As we can see in the lower part of the figure, this view has five tabs: the firs
the third the basic contracts, the fourth the advanced contracts and finally the fifth contains all specifications. the third the basic contracts, the fourth the advanced contracts and finally the fifth contains all specifications.
By clicking on the corresponding entry from the table, one can change different properties of a specification atom: the specification itself or By clicking on the corresponding entry from the table, one can change different properties of a specification atom: the specification itself or
the verification context in which this specification will be checked. the verification context in which this specification will be checked. All assumptions attached to the component selected as verification context
are taken into account when the verification is performed.
<br><br> <br><br>
<img src="./pictures/Model.Checking.Contracts.Specification.png"> <img src="./pictures/Model.Checking.Contracts.Specification.png">
......
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