// Author: heizmann@informatik.uni-freiburg.de,  Date: 5.6.2011

// Modified version of TwoThreadOneRessource-difference.ats
// Removed all transitions to accepting states and replaced 
// difference by prefixProduct.

assert(!isEmpty(prefixProduct(automaton2Net(t1), t2)));

assert(!isEmpty(prefixProduct(prefixProduct(automaton2Net(t1), t2), access2Model)));

assert(!isEmpty(prefixProduct(
    prefixProduct(
        prefixProduct(automaton2Net(t1), t2),
        access1Model),
    access2Model
)));

assert(isEmpty(prefixProduct(
    prefixProduct(
        prefixProduct(
            prefixProduct(automaton2Net(t1), t2),
            access1Model),
        access2Model),
    lockModel)
));


NestedWordAutomaton t1 = (
  callAlphabet = {},
  internalAlphabet = {"1request" "1assume2crit" "1release"},
  returnAlphabet = {},
  states = {"1idle" "1crit" "1error"},
  initialStates = {"1idle"},
  finalStates = {"1error"},
  callTransitions = {},
  internalTransitions = {("1idle" "1request" "1crit") ("1crit" "1assume2crit" "1error") ("1crit" "1release" "1idle")}, 
  returnTransitions = {}
);

NestedWordAutomaton t2 = (
  callAlphabet = {},
  internalAlphabet = {"2request" "2assume1crit" "2release"},
  returnAlphabet = {},
  states = {"2idle" "2crit" "2error"},
  initialStates = {"2idle"},
  finalStates = {"2error"},
  callTransitions = {},
  internalTransitions = {("2idle" "2request" "2crit") ("2crit" "2assume1crit" "2error") ("2crit" "2release" "2idle")}, 
  returnTransitions = {}
);

NestedWordAutomaton lockModel = (
  callAlphabet = {},
  internalAlphabet = {"1request" "1assume2crit" "1release" "2request" "2assume1crit" "2release"},
  returnAlphabet = {},
  states = {"free" "reserved" "lockFalse"},
  initialStates = {"free"},
  finalStates = {"lockFalse"},
  callTransitions = {},
  internalTransitions = {
	("free" "1request" "reserved")
	("free" "2request" "reserved")
	("free" "1release" "free")
	("free" "2release" "free")
	("free" "1assume2crit" "free")
	("free" "2assume1crit" "free")
//	("reserved" "1request" "lockFalse")
//	("reserved" "2request" "lockFalse")
	("reserved" "1release" "free")
	("reserved" "2release" "free")
	("reserved" "1assume2crit" "reserved")
	("reserved" "2assume1crit" "reserved")
//	("lockFalse" "1request" "lockFalse")
//	("lockFalse" "2request" "lockFalse")
//	("lockFalse" "1release" "lockFalse")
//	("lockFalse" "2release" "lockFalse")
//	("lockFalse" "1assume2crit" "lockFalse")
//	("lockFalse" "2assume1crit" "lockFalse")
	}, 
  returnTransitions = {}
);


NestedWordAutomaton access1Model = (
  callAlphabet = {},
  internalAlphabet = {"1request" "1assume2crit" "1release" "2request" "2assume1crit" "2release"},
  returnAlphabet = {},
  states = {"1safe" "a1crit" "a1false"},
  initialStates = {"1safe"},
  finalStates = {"a1false"},
  callTransitions = {},
  internalTransitions = {
	("1safe" "1request" "a1crit")
	("1safe" "2request" "1safe")
	("1safe" "1release" "1safe")
	("1safe" "2release" "1safe")
	("1safe" "1assume2crit" "1safe")
//	("1safe" "2assume1crit" "a1false")
	("a1crit" "1request" "a1crit")
	("a1crit" "2request" "a1crit")
	("a1crit" "1release" "1safe")
	("a1crit" "2release" "a1crit")
	("a1crit" "1assume2crit" "a1crit")
	("a1crit" "2assume1crit" "a1crit")
//	("a1false" "1request" "a1false")
//	("a1false" "2request" "a1false")
//	("a1false" "1release" "a1false")
//	("a1false" "2release" "a1false")
//	("a1false" "1assume2crit" "a1false")
//	("a1false" "2assume1crit" "a1false")
	}, 
  returnTransitions = {}
);



NestedWordAutomaton access2Model = (
  callAlphabet = {},
  internalAlphabet = {"1request" "1assume2crit" "1release" "2request" "2assume1crit" "2release"},
  returnAlphabet = {},
  states = {"2safe" "a2crit" "a2false"},
  initialStates = {"2safe"},
  finalStates = {"a2false"},
  callTransitions = {},
  internalTransitions = {
	("2safe" "1request" "2safe")
	("2safe" "2request" "a2crit")
	("2safe" "1release" "2safe")
	("2safe" "2release" "2safe")
//	("2safe" "1assume2crit" "a2false")
	("2safe" "2assume1crit" "2safe")
	("a2crit" "1request" "a2crit")
	("a2crit" "2request" "a2crit")
	("a2crit" "1release" "a2crit")
	("a2crit" "2release" "2safe")
	("a2crit" "1assume2crit" "a2crit")
	("a2crit" "2assume1crit" "a2crit")
//	("a2false" "1request" "a2false")
//	("a2false" "2request" "a2false")
//	("a2false" "1release" "a2false")
//	("a2false" "2release" "a2false")
//	("a2false" "1assume2crit" "a2false")
//	("a2false" "2assume1crit" "a2false")
	}, 
  returnTransitions = {}
);