# EDIT THE FOLLOWING by replacing the directory with your ACL2 distributed
# books directory.  You are welcome to omit this line, or not as you prefer, in
# your contribution.

include $(ACL2_SYSTEM_BOOKS)/Makefile-generic

GeNoC-departure.cert: GeNoC-departure.lisp
GeNoC-departure.cert: GeNoC-nodeset.cert
GeNoC-departure.cert: GeNoC-misc.cert
GeNoC-departure.cert: GeNoC-ntkstate.cert

GeNoC-interfaces.cert: GeNoC-interfaces.lisp
# GeNoC-interfaces.cert: $(ACL2_SYSTEM_BOOKS)/make-event/defspec.cert

GeNoC-misc.cert: GeNoC-misc.lisp
GeNoC-misc.cert: GeNoC-types.cert
# GeNoC-misc.cert: $(ACL2_SYSTEM_BOOKS)/make-event/defspec.cert

GeNoC-nodeset.cert: GeNoC-nodeset.lisp
# GeNoC-nodeset.cert: $(ACL2_SYSTEM_BOOKS)/make-event/defspec.cert

GeNoC-ntkstate.cert: GeNoC-ntkstate.lisp
GeNoC-ntkstate.cert: GeNoC-nodeset.cert
GeNoC-ntkstate.cert: GeNoC-misc.cert
GeNoC-ntkstate.cert: GeNoC-types.cert
# GeNoC-ntkstate.cert: $(ACL2_SYSTEM_BOOKS)/make-event/defspec.cert

GeNoC-priority.cert: GeNoC-priority.lisp
GeNoC-priority.cert: own-perm.cert
GeNoC-priority.cert: GeNoC-types.cert
GeNoC-priority.cert: GeNoC-misc.cert

GeNoC-routing.cert: GeNoC-routing.lisp
GeNoC-routing.cert: GeNoC-nodeset.cert
GeNoC-routing.cert: GeNoC-misc.cert
GeNoC-routing.cert: equal-ids.cert

GeNoC-scheduling.cert: GeNoC-scheduling.lisp
GeNoC-scheduling.cert: GeNoC-nodeset.cert
GeNoC-scheduling.cert: GeNoC-misc.cert
GeNoC-scheduling.cert: GeNoC-ntkstate.cert
GeNoC-scheduling.cert: wait-graph.cert
GeNoC-scheduling.cert: equal-ids.cert

GeNoC-simulation.cert: GeNoC-simulation.lisp
# GeNoC-simulation.cert: $(ACL2_SYSTEM_BOOKS)/make-event/defspec.cert

GeNoC-synchronization.cert: GeNoC-synchronization.lisp
GeNoC-synchronization.cert: GeNoC-misc.cert

GeNoC-types.cert: GeNoC-types.lisp
# GeNoC-types.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defuns.cert
# GeNoC-types.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defthms.cert

GeNoC.cert: GeNoC.lisp
GeNoC.cert: GeNoC-scheduling.cert
GeNoC.cert: GeNoC-routing.cert
GeNoC.cert: GeNoC-departure.cert
GeNoC.cert: GeNoC-simulation.cert
GeNoC.cert: interfaces-computes.cert

algorithm.cert: algorithm.lisp
algorithm.cert: nec-suff-adaptive-PS.cert
# algorithm.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/lexicographic-ordering.cert

correctness.cert: correctness.lisp
correctness.cert: algorithm.cert

dep-graph.cert: dep-graph.lisp
dep-graph.cert: graphs.cert
dep-graph.cert: generic-update-ntkstate.cert
dep-graph.cert: equal-ids.cert
dep-graph.cert: GeNoC-routing.cert

equal-ids.cert: equal-ids.lisp
equal-ids.cert: GeNoC-misc.cert
# equal-ids.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/lexicographic-ordering.cert

generic-buff-sign.cert: generic-buff-sign.lisp
generic-buff-sign.cert: GeNoC-ntkstate.cert

generic-update-ntkstate.cert: generic-update-ntkstate.lisp
generic-update-ntkstate.cert: perm.cert
generic-update-ntkstate.cert: trlstp.cert
generic-update-ntkstate.cert: generic-buff-sign.cert

graphs.cert: graphs.lisp
# graphs.cert: $(ACL2_SYSTEM_BOOKS)/make-event/defspec.cert
# graphs.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/lexicographic-ordering.cert
# graphs.cert: $(ACL2_SYSTEM_BOOKS)/data-structures/list-defthms.cert

interfaces-computes.cert: interfaces-computes.lisp
interfaces-computes.cert: GeNoC-misc.cert
interfaces-computes.cert: GeNoC-interfaces.cert

nec-suff-adaptive-PS.cert: nec-suff-adaptive-PS.lisp
nec-suff-adaptive-PS.cert: graphs.cert
nec-suff-adaptive-PS.cert: wait-graph.cert
nec-suff-adaptive-PS.cert: GeNoC.cert

own-perm.cert: own-perm.lisp
# own-perm.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/lexicographic-ordering.cert

perm.cert: perm.lisp
# perm.cert: $(ACL2_SYSTEM_BOOKS)/meta/term-defuns.cert

trlstp.cert: trlstp.lisp
trlstp.cert: GeNoC-misc.cert
trlstp.cert: perm.cert
# trlstp.cert: $(ACL2_SYSTEM_BOOKS)/ordinals/lexicographic-ordering.cert

wait-graph.cert: wait-graph.lisp
wait-graph.cert: dep-graph.cert
