Commit e72b2fa3 authored by Michael Hanus's avatar Michael Hanus
Browse files

Analysis documentation slightly extended

parent 14b8615b
......@@ -9,7 +9,8 @@ operations with a non-deterministic definition that might be called
by this operation. An operation has a non-deterministic definition
if its definition contains overlapping left-hand sides or free variables.
If the non-determinism of an operation is encapsulated
by a set function, it is considered as deterministic.
by a set function or an encapsulated search operation of the module
`AllSolutions`, it is considered as deterministic.
For instance, consider the operations
......@@ -28,3 +29,8 @@ operations `last` and `coin`. Now consider the operations
Then the operation `g` depends on the non-deterministic operation `f`,
and also on the non-deterministic operations `last` and `coin`.
In the long analysis output (produced by CASS in batch mode),
the non-deterministic operations are shown together with
the sequence of operations (limited to a length of 10)
which calls the non-deterministic operation.
......@@ -12,7 +12,8 @@ Non-deterministic operations that are called by other
non-deterministic operations are ignored so that only the first
(w.r.t. the call sequence) non-deterministic operations are returned.
Moreover, if the non-determinism of an operation is encapsulated by a
set function, it is considered as deterministic.
set function or an encapsulated search operation of the module
`AllSolutions`, it is considered as deterministic.
For instance, consider the operations
......@@ -32,3 +33,7 @@ operations `last` and `coin`. Now consider the operations
Then the operation `g` depends on the non-deterministic operation `f`,
but the dependency on the non-deterministic
operations `last` and `coin` is not reported.
In the long analysis output (produced by CASS in batch mode),
the non-deterministic operations are shown together with
the operation which directly calls the non-deterministic operation.
......@@ -126,7 +126,7 @@ maxDepsLength = 10
showNonDetDeps :: AOutFormat -> NonDetDeps -> String
showNonDetDeps AText [] = "deterministic"
showNonDetDeps ANote [] = ""
showNonDetDeps ANote xs@(_:_) = intercalate " " (map (snd . fst) xs)
showNonDetDeps ANote xs@(_:_) = intercalate " " (nub (map (snd . fst) xs))
showNonDetDeps AText xs@(_:_) =
"depends on non-det. operations: " ++
intercalate ", " (map showNDOpInfo xs)
......
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