Version 4.6.0
Version 4.6.0 provides a major update to the archive syntax and archive parsing.
- [Parser] Major update to archive syntax and parser error reporting
ArchiveEntry "Example"
Description "Illustrates the main archive syntax changes".
Definitions
Real A = 5;
Real B;
Bool inv(Real v) <-> v>=0;
End.
ProgramVariables
Real x, v; /* real-valued position and velocity */
Real a; /* current acceleration chosen by controller */
End.
Problem
A>0 & B>0 & v>=0
->
[
{
{ ?v<=5; a:=A; ++ a:=0; ++ a:=-B }
{ x'=v, v'=a & v>=0 }
}* @invariant(inv(v))
]v>=0
End.
End.
-
[Tools] Automated proof backup in plaintext archive files
-
[Tools] Improved tool stability, tool busy indicator, and tool restart and connection testing
-
[Tactics] Improved automation on typical model shapes, ODE tactic improvements