__code createTask1(struct LoopCounter* loopCounter, struct TaskManager* taskManager) { AtomicT<int>* fork0 = createAtomicTImpl<int>(contex,-1); // model checking : fork0 AtomicT<int>* fork1 = createAtomicTImpl<int>(contex,-1); // model checking : fork1 AtomicT<int>* fork2 = createAtomicTImpl<int>(contex,-1); // model checking : fork2 AtomicT<int>* fork3 = createAtomicTImpl<int>(contex,-1); // model checking : fork3 AtomicT<int>* fork4 = createAtomicTImpl<int>(contex,-1); // model checking : fork4 Phils* phils0 = createPhilsImpl(context,0,fork0,fork1); // model checking : phils0 Phils* phils1 = createPhilsImpl(context,1,fork1,fork2); // model checking : phils1 ...