// This example shows how different data (persistent/transient) is treated
// upon transaction abort.

\javaSource "code/";

\withOptions transactions:transactionsOn,
             transactionAbort:abortOn,
	     intRules:arithmeticSemanticsIgnoringOF;

\programVariables {
  MyClass self;
  int a;
}

\problem {
javacard.framework.JCSystem._transactionDepth = 0 &
!self = null & self.a = 0 & a = 0 ->
\<{
   javacard.framework.JCSystem.beginTransaction();
     self.a = 10;
     a = 10;
   javacard.framework.JCSystem.abortTransaction();
}\> (self.a = 0 & a = 10)

}