Forward countermodel construction in modal Logic K