bossBossBetterPaidThanWorker.invs bossBoss better paid than worker invariant companyHasEmployee.invs company has employee invariant hierarchyBinTree.ins hierarchy is binary tree (worker size =0 or =2) jobsAtMost.invs person has at most 2 jobs invariant percom-1.cmd 7 persons, 1 company, 7 jobs, 6 BossWorker percom-130.cmd 10 persons, 26 company, 130 jobs, 120 BossWorker percom-2.cmd 4 persons, 1 company, 4 jobs, 3 BossWorker percom-3.cmd twoRoleTC (2 persons, 3 company, 6 jobs, 4 BossWorker) percom-3b.cmd 3 persons, 2 company, 5 jobs, 3 BossWorker percom-3c.cmd 2 persons, 3 company, 2 jobs, 2 BossWorker percom-3d.cmd 26 persons, 7 company, 182 jobs, 175 BossWorker / no success percom-3e.cmd 26 persons, 4 company, 28 jobs, 24 BossWorker percom-4.cmd 4 persons, 3 company, 8 jobs, 5 BossWorker percom-5.cmd twoBossesTC (7 persons, 1 company, 7 jobs, 6 BossWorker) percom-5b.cmd 7 persons, 1 company, 7 jobs, genBW2 percom-5c.cmd 8 persons, 1 company, 8 jobs, 7 BossWorker percom-6.cmd genPersons versus genPersonsNaive percom-7.cmd bossBossVC (3 persons, 1 company, 3 jobs, bB better paid) percom-8.cmd generatePersonWith2Jobs[0|1]Companies percom-9.cmd generatePersonWith3Jobs[0|1|2]Companies percom-10.cmd generate binary tree hierarchy percom-10-X.cmd generated by 10.cmd (7P,1C,7J,6BW) percom-10-X.olt layout for percom-10-X.cmd percom-11.cmd attempt to automatically calculate reject from invs percom-12.cmd realistic snapshot (15P, 3C, 18J, 15BW) percom-13.cmd chain snapshot (7P, 1C, 7J, 6BW) percom-14.cmd 'bohling' snapshot percom.assl assl file percom.use use file personEmployeeInverseCompEmployer.invs invariant following from operation definition (VC ToDo) personWith2JobsIn0Or1Company.invs invariant not satisfiable personWith3JobsIn0Or1Or2Companies.invs invariant not satisfiable threeLevelHierarchy.cmd three level hierarchy query threeLevelHierarchy.invs three level hierarchy invariant twoBossesWithDisjointWorkers.cmd two bosses with existing disjoint workers query twoBossesWithDisjointWorkers.invs two bosses with existing disjoint workers invariant twoBossesWithDisjointWorkers2.invs two bosses with 2 disjoint workers invariant twoRoleEmployee.cmd two role employee query twoRoleEmployee.invs two role employee invariant